Merge of the "volatile" branch:

- native treatment of volatile accesses in CompCert C's semantics
- translation of volatile accesses to built-ins in SimplExpr
- native treatment of struct assignment and passing struct parameter by value
- only passing struct result by value remains emulated
- in cparser, remove emulations that are no longer used
- added C99's type _Bool and used it to express || and && more efficiently.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 15 insertions, 15 deletions

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 223d75c..e9c40a2 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -97,11 +97,11 @@ Fixpoint constval (a: expr) : res val :=
       constval r
   | Efield l f ty =>
       match typeof l with
-      | Tstruct id fList =>
+      | Tstruct id fList _ =>
           do delta <- field_offset f fList;
           do v <- constval l;
           OK (Val.add v (Vint (Int.repr delta)))
-      | Tunion id fList =>
+      | Tunion id fList _ =>
           constval l
       | _ =>
           Error(msg "ill-typed field access")
@@ -128,14 +128,14 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   do v1 <- constval a;
   do v2 <- do_cast v1 (typeof a) ty;
   match v2, ty with
-  | Vint n, Tint I8 sg => OK(Init_int8 n)
-  | Vint n, Tint I16 sg => OK(Init_int16 n)
-  | Vint n, Tint I32 sg => OK(Init_int32 n)
-  | Vint n, Tpointer _ => OK(Init_int32 n)
-  | Vfloat f, Tfloat F32 => OK(Init_float32 f)
-  | Vfloat f, Tfloat F64 => OK(Init_float64 f)
-  | Vptr (Zpos id) ofs, Tint I32 sg => OK(Init_addrof id ofs)
-  | Vptr (Zpos id) ofs, Tpointer _ => OK(Init_addrof id ofs)
+  | Vint n, Tint I8 sg _ => OK(Init_int8 n)
+  | Vint n, Tint I16 sg _ => OK(Init_int16 n)
+  | Vint n, Tint I32 sg _ => OK(Init_int32 n)
+  | Vint n, Tpointer _ _ => OK(Init_int32 n)
+  | Vfloat f, Tfloat F32 _ => OK(Init_float32 f)
+  | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
+  | Vptr (Zpos id) ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
+  | Vptr (Zpos id) ofs, Tpointer _ _ => OK(Init_addrof id ofs)
   | Vundef, _ => Error(msg "undefined operation in initializer")
   | _, _ => Error (msg "type mismatch in initializer")
   end.
@@ -152,17 +152,17 @@ Fixpoint transl_init (ty: type) (i: initializer)
   match i, ty with
   | Init_single a, _ =>
       do d <- transl_init_single ty a; OK (d :: nil)
-  | Init_compound il, Tarray tyelt sz =>
+  | Init_compound il, Tarray tyelt sz _ =>
       if zle sz 0
       then OK (Init_space(sizeof tyelt) :: nil)
       else transl_init_array tyelt il sz
-  | Init_compound il, Tstruct _ Fnil =>
+  | Init_compound il, Tstruct _ Fnil _ =>
       OK (Init_space (sizeof ty) :: nil)
-  | Init_compound il, Tstruct id fl =>
+  | Init_compound il, Tstruct id fl _ =>
       transl_init_struct id ty fl il 0
-  | Init_compound il, Tunion _ Fnil =>
+  | Init_compound il, Tunion _ Fnil _ =>
       OK (Init_space (sizeof ty) :: nil)
-  | Init_compound il, Tunion id (Fcons _ ty1 _) =>
+  | Init_compound il, Tunion id (Fcons _ ty1 _) _ =>
       transl_init_union id ty ty1 il
   | _, _ =>
       Error (msg "wrong type for compound initializer")