diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-28 08:20:14 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-03-28 08:20:14 +0000 |
| commit | c677f108ff340c5bca67b428aa6e56b47f62da8c (patch) | |
| tree | f75acecc7abe80cf06cfe01a938bdc56620137c6 /cfrontend/C2C.ml | |
| parent | f37a87e35850e57febba0a39ce3cb526e7886c10 (diff) | |
C: Support array initializers that are too short + default init for remainder.
Elab: Handle C99 designated initializers.
C2C, Initializers: more precise intermediate AST for initializers.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/C2C.ml')
| -rw-r--r-- | cfrontend/C2C.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 3f3df2e..f767372 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -123,7 +123,7 @@ let builtins_generic = { (TInt(IULongLong, []), [TPtr(TVoid [], [])], false); - "__compcert_va_int64", + "__compcert_va_float64", (TFloat(FDouble, []), [TPtr(TVoid [], [])], false) @@ -880,11 +880,11 @@ let rec convertInit env init = | C.Init_single e -> Init_single (convertExpr env e) | C.Init_array il -> - Init_compound (convertInitList env il) + Init_array (convertInitList env il) | C.Init_struct(_, flds) -> - Init_compound (convertInitList env (List.map snd flds)) + Init_struct (convertInitList env (List.map snd flds)) | C.Init_union(_, fld, i) -> - Init_compound (Init_cons(convertInit env i, Init_nil)) + Init_union (intern_string fld.fld_name, convertInit env i) and convertInitList env il = match il with |