diff options
Diffstat (limited to 'backend/Tunnelingproof.v')
| -rw-r--r-- | backend/Tunnelingproof.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 7ad75bae..49bf8942 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -297,12 +297,6 @@ Proof. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. - (* Lalloc *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_locs rs)) m'); split. - eapply exec_Lalloc; eauto. - rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. - econstructor; eauto. (* cond *) rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. left; econstructor; split. |