diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2018-09-05 17:25:56 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:59:07 +0200 |
| commit | 95926365caa7577f0936cdd4ab705d28b3d1457d (patch) | |
| tree | 198c3ed0d5ccbed5717dffdb7ce7d92454301601 /mppa_k1c/Asmgenproof.v | |
| parent | 672d9ea4489158f6a6b7175463c6514a91d1490d (diff) | |
| download | compcert-kvx-95926365caa7577f0936cdd4ab705d28b3d1457d.tar.gz compcert-kvx-95926365caa7577f0936cdd4ab705d28b3d1457d.zip | |
une solution pour le rao -> on fait remonter dans Asmblockgenproof
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 5660f718..32e8e8a8 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -50,10 +50,7 @@ Inductive code_tail: Z -> code -> code -> Prop := code_tail (pos + 1) (i :: c1) c2. Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := - forall tf tc, - Asmgen.transf_function f = OK tf -> - Asmgen.transl_code f c = OK tc -> - code_tail (Ptrofs.unsigned ofs) (fn_code tf) tc. + Asmblockgenproof.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs. Axiom return_address_exists: forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> @@ -72,7 +69,10 @@ Theorem transf_program_correct: Proof. unfold match_prog in TRANSF. simpl in TRANSF. inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. - eapply compose_forward_simulations. apply Machblockgenproof.transf_program_correct; eauto. + eapply compose_forward_simulations. + exploit Machblockgenproof.transf_program_correct; eauto. + unfold Machblockgenproof.inv_trans_rao. + intros X; apply X. eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto. apply Asm.transf_program_correct. eauto. Qed. |