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

1 files changed, 3 insertions, 4 deletions

diff --git a/backend/Mach.v b/backend/Mach.v
index c6a692a..223d5ab 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -13,8 +13,7 @@
 (** The Mach intermediate language: abstract syntax.
 
   Mach is the last intermediate language before generation of assembly
-  code.  This file defines the abstract syntax for Mach; two dynamic
-  semantics are given in modules [Machabstr] and [Machconcr].
+  code.  
 *)
 
 Require Import Coqlib.
@@ -25,6 +24,7 @@ Require Import Values.
 Require Import Memory.
 Require Import Events.
 Require Import Globalenvs.
+Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import Conventions.
@@ -40,7 +40,7 @@ Require Import Conventions.
   [Mgetstack] and [Msetstack] to read and write within the activation
   record for the current function, at a given word offset and with a
   given type; and [Mgetparam], to read within the activation record of
-  the caller.
+  the caller. 
 
   These instructions implement a more concrete view of the activation
   record than the the [Lgetstack] and [Lsetstack] instructions of
@@ -72,7 +72,6 @@ Record function: Type := mkfunction
   { fn_sig: signature;
     fn_code: code;
     fn_stacksize: Z;
-    fn_framesize: Z;
     fn_link_ofs: int;
     fn_retaddr_ofs: int }.