diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 06:39:49 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 06:39:49 +0100 |
| commit | f1a409ffe3a84f1eb6e4027a46d366a7942be0ae (patch) | |
| tree | 844145693c4e0e4a97b9834ab7b33273447104fd /backend/CSE3proof.v | |
| parent | 57345402f1f3c527defb1dc04b406d2a6aca8c72 (diff) | |
| download | compcert-kvx-f1a409ffe3a84f1eb6e4027a46d366a7942be0ae.tar.gz compcert-kvx-f1a409ffe3a84f1eb6e4027a46d366a7942be0ae.zip | |
Icall
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 9ddd6ba2..54c96cbf 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -592,7 +592,19 @@ Proof. + eapply exec_Icall; try eassumption. * TR_AT. reflexivity. * apply sig_preserved; auto. - + admit. + + rewrite subst_args_ok with (sp:=sp) (m:=m) by trivial. + assert (wt_instr f tenv (Icall (funsig fd) ros args res pc')) as WTcall by eauto with wt. + inv WTcall. + constructor; trivial. + * econstructor; eauto. + ** rewrite sig_preserved with (f:=fd); assumption. + ** intros. + IND_STEP. + apply kill_reg_sound; eauto with cse3. + eapply kill_mem_sound; eauto with cse3. + * rewrite sig_preserved with (f:=fd) by trivial. + rewrite <- H7. + apply wt_regset_list; auto. - (* Itailcall *) destruct (find_function_translated ros rs fd H0) as [tfd [HTFD1 HTFD2]]. econstructor. split. |