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, 16 insertions, 0 deletions

diff --git a/backend/Conventions.v b/backend/Conventions.v
index 9778f6a..c11bf47 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -191,6 +191,22 @@ Proof.
   intros; simpl. tauto.
 Qed.
 
+Lemma incoming_slot_in_parameters:
+  forall ofs ty sg,
+  In (S (Incoming ofs ty)) (loc_parameters sg) ->
+  In (S (Outgoing ofs ty)) (loc_arguments sg).
+Proof.
+  intros.
+  unfold loc_parameters in H. 
+  change (S (Incoming ofs ty)) with (parameter_of_argument (S (Outgoing ofs ty))) in H.
+  exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A.
+  exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros.
+  destruct x; simpl in A; try discriminate.
+  destruct s; try contradiction. 
+  inv A. auto.
+Qed. 
+
+
 (** * Tail calls *)
 
 (** A tail-call is possible for a signature if the corresponding