From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Compiler.v | 2 -- 1 file changed, 2 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index b0dce15..025b8af 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -77,7 +77,6 @@ Require Reloadproof. Require Reloadtyping. Require Stackingproof. Require Stackingtyping. -Require Machabstr2concr. Require Asmgenproof. (** Pretty-printers (defined in Caml). *) Parameter print_Csyntax: Csyntax.program -> unit. @@ -310,7 +309,6 @@ Proof. Stackingtyping.program_typing_preserved; intros. eapply Asmgenproof.transf_program_correct; eauto 6. - eapply Machabstr2concr.exec_program_equiv; eauto 6. eapply Stackingproof.transf_program_correct; eauto. eapply Reloadproof.transf_program_correct; eauto. eapply Linearizeproof.transf_program_correct; eauto. -- cgit v1.2.3