From c4f1ca931fe19f7e8e67cca6bb56dd867770d1d0 Mon Sep 17 00:00:00 2001 From: xleroy 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/Initializersproof.v | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index c2760089..c39f5f5d 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