diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-15 16:24:13 +0000 |
| commit | f774d5f2d604f747e72e2d3bb56cc3f90090e2dd (patch) | |
| tree | 05a5bcfc207c67f58575fa7b61787c0c9dbe8215 /backend/Inliningproof.v | |
| parent | f1ceca440c0322001abe6c5de79bd4bc309fc002 (diff) | |
| download | compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.tar.gz compcert-kvx-f774d5f2d604f747e72e2d3bb56cc3f90090e2dd.zip | |
Pointers one past
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 9536141a..ba61ed09 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'). |