From 3f1fb601a23c63eb5c619330c632b6f2dba36ad7 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 16 Sep 2006 08:56:15 +0000 Subject: 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 --- caml/Cil2Csyntax.ml | 14 +++++++++----- 1 file 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"; -- cgit