diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-28 13:59:55 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-28 13:59:55 +0100 |
| commit | 5412aea57eafe2868244a514471d480b83fc51bd (patch) | |
| tree | 1fcca72f850293171c49ad9560001ce9e89f1354 /backend/CSE2proof.v | |
| parent | 47bcd22f7e1febf10bd0629c1774b7ab39fac872 (diff) | |
| download | compcert-kvx-5412aea57eafe2868244a514471d480b83fc51bd.tar.gz compcert-kvx-5412aea57eafe2868244a514471d480b83fc51bd.zip | |
connected (just a silly problem)
Diffstat (limited to 'backend/CSE2proof.v')
| -rw-r--r-- | backend/CSE2proof.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v index 558490ba..1d0a617a 100644 --- a/backend/CSE2proof.v +++ b/backend/CSE2proof.v @@ -405,7 +405,6 @@ Lemma kill_reg_weaken: sem_rel mpc rs -> sem_rel (kill_reg res mpc) rs. Proof. - Check kill_reg_sound. intros until rs. intros REL x. pose proof (REL x) as RELx. @@ -471,6 +470,14 @@ Qed. End SOUNDNESS. +Definition match_prog (p tp: RTL.program) := + match_program (fun cu f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: + forall p, match_prog p (transf_program p). +Proof. + intros. apply match_transform_program; auto. +Qed. Section PRESERVATION. @@ -849,7 +856,6 @@ Proof. eapply exec_Itailcall with (fd := transf_fundef fd); eauto. eapply find_function_translated; eauto. apply sig_preserved. - Check subst_args_ok. rewrite (subst_args_ok' (Vptr stk Ptrofs.zero) m) by assumption. constructor. auto. |