diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 16:25:25 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 16:25:25 +0200 |
commit | 170284b51766112e29d6bbfe519bad9f6da95269 (patch) | |
tree | 13a163ccee48cee0512a8af484b394623cdce030 /backend/CSEproof.v | |
parent | 2e30ad9698a6f24a8a746f68b30c235913006392 (diff) | |
parent | 959432fa13a899290db5236f93575a8bfdc13bb5 (diff) | |
download | compcert-kvx-170284b51766112e29d6bbfe519bad9f6da95269.tar.gz compcert-kvx-170284b51766112e29d6bbfe519bad9f6da95269.zip |
Merge branch 'master' into dwarf
Diffstat (limited to 'backend/CSEproof.v')
-rw-r--r-- | backend/CSEproof.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index ae8052be..74e3ceca 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1144,6 +1144,21 @@ Proof. + apply CASE1. * apply set_reg_lessdef; auto. +- (* Iannot *) + exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. + intros (vargs' & A & B). + exploit external_call_mem_extends; eauto. + intros (v' & m1' & P & Q & R & S). + econstructor; split. + eapply exec_Iannot; eauto. + eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. + econstructor; eauto. + eapply analysis_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. replace m' with m; auto. + destruct ef; try contradiction. inv H2; auto. + - (* Icond *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. elim SAT; intros valu1 NH1. |