diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:04:52 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-14 08:04:52 +0100 |
| commit | 74fef42251167061e7fd863ac2bb06bb6e58d3d4 (patch) | |
| tree | 78c6255324358e4c8c13047cb67208a2c4942e4a /backend/CSE3proof.v | |
| parent | 71a3e11b500713b53f13fe64b87ebeb1c9c6e312 (diff) | |
| download | compcert-kvx-74fef42251167061e7fd863ac2bb06bb6e58d3d4.tar.gz compcert-kvx-74fef42251167061e7fd863ac2bb06bb6e58d3d4.zip | |
Ireturn
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index cd129cb2..2a33fa1c 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -661,16 +661,16 @@ Proof. IND_STEP. - (* Ireturn *) - destruct or. + destruct or as [arg | ]. -- econstructor. split. - + eapply exec_Ireturn; try eassumption. - * erewrite transf_function_at by eauto. simpl. - admit. + + eapply exec_Ireturn with (or := Some (subst_arg (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc arg)). + * TR_AT. reflexivity. * rewrite stacksize_preserved with (f:=f); eauto. - + econstructor; eauto. - simpl. + + simpl. + rewrite subst_arg_ok with (sp:=(Vptr stk Ptrofs.zero)) (m:=m) by trivial. + econstructor; eauto. apply type_function_correct in WTF. - apply wt_instrs with (pc:=pc) (instr:=(Ireturn (Some r))) in WTF. + apply wt_instrs with (pc:=pc) (instr:=(Ireturn (Some arg))) in WTF. 2: assumption. inv WTF. rewrite sig_preserved2 with (f:=f) by assumption. |