diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:19:22 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:19:22 +0200 |
| commit | c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 (patch) | |
| tree | e63d0437c3f3cb43eb26cced8ad94acc62e82dad /backend/Bounds.v | |
| parent | 7042070a3668ae149ec6a490b8e7c1a6aa82d6fe (diff) | |
| download | compcert-kvx-c4cc75dc6abcb0eee6f3288e96fea4aec540fd68.tar.gz compcert-kvx-c4cc75dc6abcb0eee6f3288e96fea4aec540fd68.zip | |
more proofs going through
Diffstat (limited to 'backend/Bounds.v')
| -rw-r--r-- | backend/Bounds.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index fa695234..b8c12166 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -67,7 +67,7 @@ Definition instr_within_bounds (i: instruction) := | Lgetstack sl ofs ty r => slot_within_bounds sl ofs ty /\ mreg_within_bounds r | Lsetstack r sl ofs ty => slot_within_bounds sl ofs ty | Lop op args res => mreg_within_bounds res - | Lload chunk addr args dst => mreg_within_bounds dst + | Lload trap chunk addr args dst => mreg_within_bounds dst | Lcall sig ros => size_arguments sig <= bound_outgoing b | Lbuiltin ef args res => (forall r, In r (params_of_builtin_res res) \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r) @@ -104,7 +104,7 @@ Definition record_regs_of_instr (u: RegSet.t) (i: instruction) : RegSet.t := | Lgetstack sl ofs ty r => record_reg u r | Lsetstack r sl ofs ty => record_reg u r | Lop op args res => record_reg u res - | Lload chunk addr args dst => record_reg u dst + | Lload trap chunk addr args dst => record_reg u dst | Lstore chunk addr args src => u | Lcall sig ros => u | Ltailcall sig ros => u @@ -280,7 +280,7 @@ Definition defined_by_instr (r': mreg) (i: instruction) := match i with | Lgetstack sl ofs ty r => r' = r | Lop op args res => r' = res - | Lload chunk addr args dst => r' = dst + | Lload trap chunk addr args dst => r' = dst | Lbuiltin ef args res => In r' (params_of_builtin_res res) \/ In r' (destroyed_by_builtin ef) | _ => False end. |