From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 11 Jan 2009 11:57:02 +0000 Subject: - Added alignment constraints to memory loads and stores. - In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Tunnelingproof.v | 6 ------ 1 file changed, 6 deletions(-) (limited to 'backend/Tunnelingproof.v') 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. -- cgit