diff options
Diffstat (limited to 'cfrontend/Initializers.v')
| -rw-r--r-- | cfrontend/Initializers.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 8757ba2e..7711adea 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -151,10 +151,12 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data := | 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) + | Vint n, Tcomp_ptr _ _ => 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) + | Vptr (Zpos id) ofs, Tcomp_ptr _ _ => OK(Init_addrof id ofs) | Vundef, _ => Error(msg "undefined operation in initializer") | _, _ => Error (msg "type mismatch in initializer") end. @@ -208,7 +210,7 @@ with transl_init_struct (id: ident) (ty: type) OK (padding pos (sizeof ty)) | Init_cons i1 il', Fcons _ ty1 fl' => let pos1 := align pos (alignof ty1) in - do d1 <- transl_init (unroll_composite id ty ty1) i1; + do d1 <- transl_init ty1 i1; do d2 <- transl_init_struct id ty fl' il' (pos1 + sizeof ty1); OK (padding pos pos1 ++ d1 ++ d2) | _, _ => @@ -221,7 +223,7 @@ with transl_init_union (id: ident) (ty ty1: type) (il: initializer_list) | Init_nil => Error (msg "empty union initializer") | Init_cons i1 _ => - do d <- transl_init (unroll_composite id ty ty1) i1; + do d <- transl_init ty1 i1; OK (d ++ padding (sizeof ty1) (sizeof ty)) end. |