From 5a632954c85e8b2b5afea124e4fc83f39c5d3598 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 1 Jun 2021 14:37:07 +0200
Subject: [BROKEN] Merge with v3.9 : something broken for __builtin_expect in
 cfrontend/C2C.ml

---
 powerpc/Asm.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'powerpc/Asm.v')

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 93bc31b8..6b1f2232 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -538,6 +538,8 @@ Axiom small_data_area_addressing:
 
 Parameter symbol_is_rel_data: ident -> ptrofs -> bool.
 
+Parameter symbol_is_aligned: ident -> Z -> bool.
+
 (** Armed with the [low_half] and [high_half] functions,
   we can define the evaluation of a symbolic constant.
   Note that for [const_high], integer constants
-- 
cgit