From f774d5f2d604f747e72e2d3bb56cc3f90090e2dd Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 15 Feb 2013 16:24:13 +0000 Subject: Pointers one past git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Inlining.v | 2 +- backend/Inliningproof.v | 10 +++++----- backend/Inliningspec.v | 4 ++-- backend/Reloadtyping.v | 5 +---- 4 files changed, 9 insertions(+), 12 deletions(-) (limited to 'backend') 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. -- cgit v1.2.3