From 25b9b003178002360d666919f2e49e7f5f4a36e2 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Feb 2012 19:14:14 +0000 Subject: 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 --- cfrontend/Initializers.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'cfrontend/Initializers.v') 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") -- cgit v1.2.3