diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-12 12:55:21 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-12 12:55:21 +0000 |
| commit | aaa49526068f528f2233de0dace43549432fba52 (patch) | |
| tree | e675fe11f225858ddd290594fa5ffed2865d5677 /backend/Bounds.v | |
| parent | 845148dea58bbdd041c399a8c9196d9e67bec629 (diff) | |
| download | compcert-kvx-aaa49526068f528f2233de0dace43549432fba52.tar.gz compcert-kvx-aaa49526068f528f2233de0dace43549432fba52.zip | |
Revu gestion retaddr et link dans Stacking
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Bounds.v')
| -rw-r--r-- | backend/Bounds.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 0e8b9faf..415a85f0 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -63,7 +63,7 @@ Definition slot_within_bounds (s: slot) := | Local ofs Tint => 0 <= ofs < bound_int_local b | Local ofs Tfloat => 0 <= ofs < bound_float_local b | Outgoing ofs ty => 14 <= ofs /\ ofs + typesize ty <= bound_outgoing b - | Incoming ofs ty => 14 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig) + | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig)) end. Definition instr_within_bounds (i: instruction) := |