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 /cparser/Unblock.ml | |
parent | f37a87e35850e57febba0a39ce3cb526e7886c10 (diff) | |
download | compcert-c677f108ff340c5bca67b428aa6e56b47f62da8c.tar.gz compcert-c677f108ff340c5bca67b428aa6e56b47f62da8c.zip |
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 'cparser/Unblock.ml')
-rw-r--r-- | cparser/Unblock.ml | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index c40da18e..34d8cf8e 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -35,19 +35,23 @@ let rec local_initializer loc env path init k = { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp } k | Init_array il -> - let ty_elt = + let (ty_elt, sz) = match unroll env path.etyp with - | TArray(ty_elt, _, _) -> ty_elt + | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) | _ -> fatal_error "%aWrong type for array initializer" formatloc loc in - let rec array_init pos = function - | [] -> k - | i :: il -> - local_initializer loc env - { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, [])); - etyp = ty_elt } - i - (array_init (Int64.succ pos) il) in + let rec array_init pos il = + if pos >= sz then k else begin + let (i1, il') = + match il with + | [] -> (default_init env ty_elt, []) + | i1 :: il' -> (i1, il') in + local_initializer loc env + { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, [])); + etyp = ty_elt } + i1 + (array_init (Int64.succ pos) il') + end in array_init 0L il | Init_struct(id, fil) -> let field_init (fld, i) k = |