From c4f1ca931fe19f7e8e67cca6bb56dd867770d1d0 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 18 Mar 2014 10:31:11 +0000
Subject: Support array initialization lists that are too short

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2432 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Initializers.v      |  4 ++--
 cfrontend/Initializersproof.v | 16 ++++++++++++----
 2 files changed, 14 insertions(+), 6 deletions(-)

(limited to 'cfrontend')

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 1b339c1..f180f98 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -190,8 +190,8 @@ with transl_init_array (ty: type) (il: initializer_list) (sz: Z)
                        {struct il} : res (list init_data) :=
   match il with
   | Init_nil =>
-      if zeq sz 0
-      then OK nil
+      if zeq sz 0 then OK nil
+      else if zle 0 sz then OK (Init_space (sz * sizeof ty) :: nil)
       else Error (msg "wrong number of elements in array initializer")
   | Init_cons i1 il' =>
       do d1 <- transl_init ty i1;
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index c276008..c39f5f5 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -606,7 +606,12 @@ Local Opaque alignof.
 + (* base cases *)
   simpl. intuition. 
 * (* arrays *)
-  destruct (zeq sz 0); inv H. simpl. ring. 
+  destruct (zeq sz 0).  inv H.  simpl; ring. 
+  destruct (zle 0 sz);  inv H.  simpl. 
+  rewrite Z.mul_comm. 
+  assert (0 <= sizeof ty * sz).
+  { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ty); omega. }
+  zify; omega.
 * (* structs *)
   destruct fl; inv H.
   simpl in H0. rewrite padding_size by omega. omega. 
@@ -665,8 +670,9 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
       exec_init m b ofs (Tunion id (Fcons id1 ty1 fl) a) (Init_compound (Init_cons i Init_nil)) m'
 
 with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop :=
-  | exec_init_array_nil: forall m b ofs ty,
-      exec_init_array m b ofs ty 0 Init_nil m
+  | exec_init_array_nil: forall m b ofs ty sz,
+      sz >= 0 ->
+      exec_init_array m b ofs ty sz Init_nil m
   | exec_init_array_cons: forall m b ofs ty sz i1 il m' m'',
       exec_init m b ofs ty i1 m' ->
       exec_init_array m' b (ofs + sizeof ty) ty (sz - 1) il m'' ->
@@ -738,7 +744,9 @@ Local Opaque sizeof.
   apply store_init_data_list_padding. 
 
 - (* array, empty *)
-  inv H. auto.
+  destruct (zeq sz 0).
+  inv H0. auto.
+  rewrite zle_true in H0 by omega. inv H0. auto.
 - (* array, nonempty *)
   monadInv H3. 
   eapply store_init_data_list_app.
-- 
cgit v1.2.3