diff options
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. } |