diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-16 08:56:15 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-16 08:56:15 +0000 |
commit | 3f1fb601a23c63eb5c619330c632b6f2dba36ad7 (patch) | |
tree | 54de1e2c984de54ce27d5ad66ea7e8bc9e1fb0a9 /caml | |
parent | 9d125a3c856d891b234cec1a24264ba72659c18f (diff) | |
download | compcert-3f1fb601a23c63eb5c619330c632b6f2dba36ad7.tar.gz compcert-3f1fb601a23c63eb5c619330c632b6f2dba36ad7.zip |
Const.prop dans la taille des tableaux. Tolerer (avec warning) les declarations extern ty var[].
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@100 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
-rw-r--r-- | caml/Cil2Csyntax.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index 85f3b186..c0e4837f 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -404,11 +404,15 @@ and convertTypGen env = function | TPtr (t, _) -> Tpointer (convertTypGen env t) | TArray (t, eOpt, _) -> begin match eOpt with - | Some (Const (CInt64 (i64, _, _))) -> - Tarray (convertTypGen env t, - coqint_of_camlint (Int64.to_int32 i64)) - | Some _ -> unsupported "size of array type not an integer constant" - | None -> unsupported "array type of unspecified size" + | None -> + warning "array type of unspecified size"; + Tarray (convertTypGen env t, coqint_of_camlint 0l) + | Some e -> + match Cil.constFold true e with + | Const (CInt64 (i64, _, _)) -> + Tarray (convertTypGen env t, + coqint_of_camlint (Int64.to_int32 i64)) + | _ -> unsupported "size of array type not an integer constant" end | TFun (t, argListOpt, vArg, _) -> if vArg then unsupported "variadic function type"; |