diff options
Diffstat (limited to 'backend/Tailcallproof.v')
| -rw-r--r-- | backend/Tailcallproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 80a68327..39fc10fb 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -440,7 +440,7 @@ Proof. TransfInstr. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto. left. - exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split. + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. eapply exec_Iload_notrap1. eassumption. eapply eval_addressing_lessdef_none. eassumption. @@ -465,7 +465,7 @@ Proof. exact symbols_preserved. assumption. econstructor; eauto. apply set_reg_lessdef; auto. - + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- (default_notrap_load_value chunk)) m'); split. + + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split. eapply exec_Iload_notrap2. eassumption. erewrite eval_addressing_preserved. eassumption. |