diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-11 11:41:37 +0200 |
commit | af16cdae6d58033cc8aa06bca330f98b96ba12f2 (patch) | |
tree | 4985e9ae8fa0d580bbf95a198edeca4f0bd6ff46 /cfrontend/Initializersproof.v | |
parent | 21c979fce33b068ce4b86e67d3d866b203411c6c (diff) | |
parent | 02b169b444c435b8d1aacf54969dd7de57317a5c (diff) | |
download | compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.tar.gz compcert-kvx-af16cdae6d58033cc8aa06bca330f98b96ba12f2.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'cfrontend/Initializersproof.v')
-rw-r--r-- | cfrontend/Initializersproof.v | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 272b929f..10ccbeff 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -561,7 +561,7 @@ Local Opaque sizeof. + destruct (zeq sz 0). inv TR. exists (@nil init_data); split; auto. constructor. destruct (zle 0 sz). - inv TR. econstructor; split. constructor. omega. auto. + inv TR. econstructor; split. constructor. lia. auto. discriminate. + monadInv TR. destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1). @@ -672,8 +672,8 @@ Remark padding_size: forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm. Proof. unfold tr_padding; intros. destruct (zlt frm to). - simpl. xomega. - simpl. omega. + simpl. extlia. + simpl. lia. Qed. Remark idlsize_app: @@ -681,7 +681,7 @@ Remark idlsize_app: Proof. induction d1; simpl; intros. auto. - rewrite IHd1. omega. + rewrite IHd1. lia. Qed. Remark union_field_size: @@ -690,8 +690,8 @@ Proof. induction fl as [|[i t]]; simpl; intros. - inv H. - destruct (ident_eq f i). - + inv H. xomega. - + specialize (IHfl H). xomega. + + inv H. extlia. + + specialize (IHfl H). extlia. Qed. Hypothesis ce_consistent: composite_env_consistent ge. @@ -712,16 +712,16 @@ with tr_init_struct_size: Proof. Local Opaque sizeof. - destruct 1; simpl. -+ erewrite transl_init_single_size by eauto. omega. ++ erewrite transl_init_single_size by eauto. lia. + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. -+ replace (idlsize d) with (idlsize d + 0) by omega. ++ replace (idlsize d) with (idlsize d + 0) by lia. eapply tr_init_struct_size; eauto. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite H0. apply align_le. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + rewrite idlsize_app, padding_size. - exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. + exploit tr_init_size; eauto. intros EQ; rewrite EQ. lia. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. apply Z.le_trans with (sizeof_union ge (co_members co)). eapply union_field_size; eauto. @@ -730,21 +730,21 @@ Local Opaque sizeof. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. - destruct 1; simpl. -+ omega. ++ lia. + rewrite Z.mul_comm. assert (0 <= sizeof ge ty * sz). - { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } - xomega. + { apply Zmult_gt_0_le_0_compat. lia. generalize (sizeof_pos ge ty); lia. } + extlia. + rewrite idlsize_app. erewrite tr_init_size by eauto. erewrite tr_init_array_size by eauto. ring. - destruct 1; simpl; intros. -+ rewrite padding_size by auto. omega. ++ rewrite padding_size by auto. lia. + rewrite ! idlsize_app, padding_size. erewrite tr_init_size by eauto. - rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega. + rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). lia. unfold pos1. apply align_le. apply alignof_pos. Qed. @@ -806,7 +806,7 @@ Remark exec_init_array_length: forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' -> sz >= 0. Proof. - induction 1; omega. + induction 1; lia. Qed. Lemma store_init_data_list_app: @@ -847,10 +847,10 @@ Local Opaque sizeof. inv H3. simpl. erewrite transl_init_single_steps by eauto. auto. - (* array *) inv H1. replace (Z.max 0 sz) with sz in H7. eauto. - assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. + assert (sz >= 0) by (eapply exec_init_array_length; eauto). extlia. - (* struct *) inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. - replace ofs with (ofs + 0) by omega. eauto. + replace ofs with (ofs + 0) by lia. eauto. - (* union *) inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. eapply store_init_data_list_app. eauto. @@ -870,7 +870,7 @@ Local Opaque sizeof. inv H4. simpl in H3; inv H3. eapply store_init_data_list_app. apply store_init_data_list_padding. rewrite padding_size. - replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega. + replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by lia. eapply store_init_data_list_app. eauto. rewrite (tr_init_size _ _ _ H9). |