diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-19 18:01:10 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-19 18:01:10 +0100 |
| commit | f0a218800bf0b8a94da35fd8a0553184294f6368 (patch) | |
| tree | ccbccb6d3766930091f40264393cda1003c810a8 /aarch64/Asmblockgenproof.v | |
| parent | 95dc0730b9fa0f7d60222f53d7cdc3aed14206da (diff) | |
| download | compcert-kvx-f0a218800bf0b8a94da35fd8a0553184294f6368.tar.gz compcert-kvx-f0a218800bf0b8a94da35fd8a0553184294f6368.zip | |
Asmblockgenproof finished !
Diffstat (limited to 'aarch64/Asmblockgenproof.v')
| -rw-r--r-- | aarch64/Asmblockgenproof.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 586286bd..1abcb570 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -77,11 +77,6 @@ Qed. Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. -(*Lemma functions_bound_max_pos: forall fb f, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - (max_pos next f) <= Ptrofs.max_unsigned. -Admitted.*) - (** * Proof of semantic preservation *) (** Semantic preservation is proved using a complex simulation diagram @@ -881,7 +876,7 @@ exploit builtin_args_match; eauto. intros [vargs' [P Q]]. eapply preg_vals; eauto. all: eauto. intros EC. - exploit transl_cbranch_correct_true; eauto. intros (rs', H). + exploit transl_cbranch_correct_1; eauto. intros (rs', H). destruct H as [ES [ECFI]]. exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } @@ -909,7 +904,7 @@ exploit builtin_args_match; eauto. intros [vargs' [P Q]]. all: eauto. intros EC. - exploit transl_cbranch_correct_false; eauto. intros (rs', H). + exploit transl_cbranch_correct_1; eauto. intros (rs', H). destruct H as [ES [ECFI]]. exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } |