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, 9 insertions, 3 deletions

diff --git a/backend/Bounds.v b/backend/Bounds.v
index 514895b..0415670 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -10,7 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(** Computation of resource bounds forr Linear code. *)
+(** Computation of resource bounds for Linear code. *)
 
 Require Import Coqlib.
 Require Import Maps.
@@ -36,11 +36,13 @@ Record bounds : Type := mkbounds {
   bound_int_callee_save: Z;
   bound_float_callee_save: Z;
   bound_outgoing: Z;
+  bound_stack_data: Z;
   bound_int_local_pos: bound_int_local >= 0;
   bound_float_local_pos: bound_float_local >= 0;
   bound_int_callee_save_pos: bound_int_callee_save >= 0;
   bound_float_callee_save_pos: bound_float_callee_save >= 0;
-  bound_outgoing_pos: bound_outgoing >= 0
+  bound_outgoing_pos: bound_outgoing >= 0;
+  bound_stack_data_pos: bound_stack_data >= 0
 }.
 
 (** The following predicates define the correctness of a set of bounds
@@ -186,15 +188,19 @@ Program Definition function_bounds :=
     (max_over_regs_of_funct float_callee_save)
     (Zmax (max_over_instrs outgoing_space)
           (max_over_slots_of_funct outgoing_slot))
+    (Zmax f.(fn_stacksize) 0)
     (max_over_slots_of_funct_pos int_local)
     (max_over_slots_of_funct_pos float_local)
     (max_over_regs_of_funct_pos int_callee_save)
     (max_over_regs_of_funct_pos float_callee_save)
-    _.
+    _ _.
 Next Obligation.
   apply Zle_ge. eapply Zle_trans. 2: apply Zmax2.
   apply Zge_le. apply max_over_slots_of_funct_pos.  
 Qed.
+Next Obligation.
+  apply Zle_ge. apply Zmax2.
+Qed.
 
 (** We now show the correctness of the inferred bounds. *)