[BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend/C2C.ml

4 files changed, 46 insertions, 28 deletions

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 8af920df..708be1cb 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -6,10 +6,11 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -18,6 +19,8 @@
 From Coq Require Import Ascii String List ZArith.
 From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight.
 
+(** ** Short names for types *)
+
 Definition tvoid := Tvoid.
 Definition tschar := Tint I8 Signed noattr.
 Definition tuchar := Tint I8 Unsigned noattr.
@@ -56,6 +59,8 @@ Definition talignas (n: N) (ty: type) :=
 Definition tvolatile_alignas (n: N) (ty: type) :=
   tattr {| attr_volatile := true; attr_alignas := Some n |} ty.
 
+(** ** Constructor for programs and compilation units *)
+
 Definition wf_composites (types: list composite_definition) : Prop :=
   match build_composite_env types with OK _ => True | Error _ => False end.
 
@@ -81,6 +86,8 @@ Definition mkprogram (types: list composite_definition)
      prog_comp_env := ce;
      prog_comp_env_eq := EQ |}.
 
+(** ** Encoding character strings as positive numbers *)
+
 (** The following encoding of character strings as positive numbers
     must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *)
 
@@ -169,17 +176,6 @@ Fixpoint ident_of_string (s: string) : ident :=
   | String c s => append_char_pos c (ident_of_string s)
   end.
 
-(** A convenient notation [$ "ident"] to force evaluation of
-    [ident_of_string "ident"] *)
-
-Ltac ident_of_string s :=
-  let x := constr:(ident_of_string s) in
-  let y := eval compute in x in
-  exact y.
-
-Notation "$ s" := (ltac:(ident_of_string s))
-                  (at level 1, only parsing) : string_scope.
-
 (** The inverse conversion, from encoded strings to strings *)
 
 Section DECODE_BITS.
@@ -289,3 +285,20 @@ Proof.
   intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2).
   congruence.
 Qed.
+
+(** ** Notations *)
+
+Module ClightNotations.
+
+(** A convenient notation [$ "ident"] to force evaluation of
+    [ident_of_string "ident"] *)
+
+Ltac ident_of_string s :=
+  let x := constr:(ident_of_string s) in
+  let y := eval compute in x in
+  exact y.
+
+Notation "$ s" := (ltac:(ident_of_string s))
+                  (at level 1, only parsing) : clight_scope.
+
+End ClightNotations.
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 5e27370e..44c76cc6 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -6,10 +6,11 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/exportclight/Clightnorm.ml b/exportclight/Clightnorm.ml
index a6158b60..88d44c08 100644
--- a/exportclight/Clightnorm.ml
+++ b/exportclight/Clightnorm.ml
@@ -6,10 +6,11 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 7604175e..474a1bd8 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -6,10 +6,11 @@
 (*                                                                     *)
 (*  Copyright Institut National de Recherche en Informatique et en     *)
 (*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*  under the terms of the GNU Lesser General Public License as        *)
+(*  published by the Free Software Foundation, either version 2.1 of   *)
+(*  the License, or  (at your option) any later version.               *)
+(*  This file is also distributed under the terms of the               *)
+(*  INRIA Non-Commercial License Agreement.                            *)
 (*                                                                     *)
 (* *********************************************************************)
 
@@ -455,8 +456,10 @@ let print_composite_definition p (Composite(id, su, m, a)) =
 let prologue = "\
 From Coq Require Import String List ZArith.\n\
 From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\
+Import Clightdefs.ClightNotations.\n\
 Local Open Scope Z_scope.\n\
-Local Open Scope string_scope.\n"
+Local Open Scope string_scope.\n\
+Local Open Scope clight_scope.\n"
 
 (* Naming the compiler-generated temporaries occurring in the program *)