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/Inliningspec.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/Inliningspec.v')
| -rw-r--r-- | backend/Inliningspec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 06826c24..82ef9cf9 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. |