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

1 files changed, 9 insertions, 5 deletions

diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml
index 85f3b18..c0e4837 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";