diff options
Diffstat (limited to 'backend/Tailcallproof.v')
| -rw-r--r-- | backend/Tailcallproof.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 06e314f3..4a5e83a1 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -438,6 +438,19 @@ Proof. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply set_reg_lessdef; auto. + (* TODO *) +- (* load notrap1 *) + TransfInstr. + assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. + + intros [a' [ADDR' ALD]]. + exploit Mem.loadv_extends; eauto. + intros [v' [LOAD' VLD]]. + left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split. + eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. + apply eval_addressing_preserved. exact symbols_preserved. eauto. + econstructor; eauto. apply set_reg_lessdef; auto. + - (* store *) TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. |