diff options
Diffstat (limited to 'backend/Tunnelingproof.v')
| -rw-r--r-- | backend/Tunnelingproof.v | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index c6644ceb..4f95ac9b 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -334,6 +334,16 @@ Proof. induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef. Qed. +Lemma locmap_undef_caller_save_regs_lessdef: + forall ls1 ls2, + locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_caller_save_regs ls1) (undef_caller_save_regs ls2). +Proof. + intros; red; intros. unfold undef_caller_save_regs. + destruct l. +- destruct (Conventions1.is_callee_save r); auto. +- destruct sl; auto. +Qed. + Lemma find_function_translated: forall ros ls tls fd, locmap_lessdef ls tls -> @@ -363,7 +373,7 @@ Lemma return_regs_lessdef: Proof. intros; red; intros. destruct l; simpl. - destruct (Conventions1.is_callee_save r); auto. -- auto. +- destruct sl; auto. Qed. (** To preserve non-terminating behaviours, we show that the transformed @@ -516,7 +526,7 @@ Proof. left; simpl; econstructor; split. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. - simpl. econstructor; eauto using locmap_setpair_lessdef. + simpl. econstructor; eauto using locmap_setpair_lessdef, locmap_undef_caller_save_regs_lessdef. - (* return *) inv STK. inv H1. left; econstructor; split. |