Pointers one past

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 9 insertions, 12 deletions

diff --git a/backend/Inlining.v b/backend/Inlining.v
index 5075fd6..a9b1e7e 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -454,7 +454,7 @@ Local Open Scope string_scope.
 
 Definition transf_function (fenv: funenv) (f: function) : Errors.res function :=
   let '(R ctx s _) := expand_function fenv f initstate in
-  if zle s.(st_stksize) Int.max_unsigned then
+  if zlt s.(st_stksize) Int.max_unsigned then
     OK (mkfunction f.(fn_sig) 
                    (sregs ctx f.(fn_params))
                    s.(st_stksize)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 9536141..ba61ed0 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -398,7 +398,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
         (AG: agree_regs F ctx rs rs')
         (SP: F sp = Some(sp', ctx.(dstk)))
         (PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RES: Ple res ctx.(mreg))
         (BELOW: sp' < bound),
@@ -409,7 +409,7 @@ Inductive match_stacks (F: meminj) (m m': mem):
   | match_stacks_untailcall: forall stk res f' sp' rpc rs' stk' bound ctx
         (MS: match_stacks_inside F m m' stk stk' f' ctx sp' rs')
         (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize))
         (RET: ctx.(retinfo) = Some (rpc, res))
         (BELOW: sp' < bound),
@@ -775,7 +775,7 @@ Inductive match_states: state -> state -> Prop :=
         (MINJ: Mem.inject F m m')
         (VB: Mem.valid_block m' sp')
         (PRIV: range_private F m m' sp' (ctx.(dstk) + ctx.(mstk)) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
       match_states (State stk f (Vptr sp Int.zero) pc rs m)
                    (State stk' f' (Vptr sp' Int.zero) (spc ctx pc) rs' m')
@@ -796,7 +796,7 @@ Inductive match_states: state -> state -> Prop :=
         (MINJ: Mem.inject F m m')
         (VB: Mem.valid_block m' sp')
         (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
       match_states (Callstate stk (Internal f) vargs m)
                    (State stk' f' (Vptr sp' Int.zero) pc' rs' m')
@@ -814,7 +814,7 @@ Inductive match_states: state -> state -> Prop :=
         (MINJ: Mem.inject F m m')
         (VB: Mem.valid_block m' sp')
         (PRIV: range_private F m m' sp' ctx.(dstk) f'.(fn_stacksize))
-        (SSZ1: 0 <= f'.(fn_stacksize) <= Int.max_unsigned)
+        (SSZ1: 0 <= f'.(fn_stacksize) < Int.max_unsigned)
         (SSZ2: forall ofs, Mem.perm m' sp' ofs Max Nonempty -> 0 <= ofs <= f'.(fn_stacksize)),
       match_states (Returnstate stk v m)
                    (State stk' f' (Vptr sp' Int.zero) pc' rs' m').
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index 06826c2..82ef9cf 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -664,7 +664,7 @@ Inductive tr_function: function -> function -> Prop :=
       f'.(fn_sig) = f.(fn_sig) ->
       f'.(fn_params) = sregs ctx f.(fn_params) ->
       f'.(fn_entrypoint) = spc ctx f.(fn_entrypoint) ->
-      0 <= fn_stacksize f' <= Int.max_unsigned ->
+      0 <= fn_stacksize f' < Int.max_unsigned ->
       tr_function f f'.
 
 Lemma transf_function_spec:
@@ -672,7 +672,7 @@ Lemma transf_function_spec:
 Proof.
   intros. unfold transf_function in H.
   destruct (expand_function fenv f initstate) as [ctx s i] eqn:?. 
-  destruct (zle (st_stksize s) Int.max_unsigned); inv H.
+  destruct (zlt (st_stksize s) Int.max_unsigned); inv H.
   monadInv Heqr. set (ctx := initcontext x x0 (max_def_function f) (fn_stacksize f)) in *.
 Opaque initstate.
   destruct INCR3. inversion EQ1. inversion EQ.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 9f5563c..c005139 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -288,8 +288,7 @@ Proof.
     rewrite loc_arguments_type; auto.
   destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. 
   auto 10 with reloadty.
-
-  destruct (ef_reloads ef) as [] eqn:?.
+  destruct (ef_reloads ef) eqn:?.
   assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence.
   assert (map mreg_type (regs_for args) = map Loc.type args).
     apply wt_regs_for. apply arity_ok_enough. congruence.
@@ -297,8 +296,6 @@ Proof.
   auto 10 with reloadty.
   auto with reloadty.
 
-
-
   assert (map mreg_type (regs_for args) = map Loc.type args).
     eauto with reloadty.
   auto with reloadty.