diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 17:23:41 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-02-04 17:23:41 +0100 |
| commit | b55e522ca286bbe96be3ce5fc05c984b2a4a130a (patch) | |
| tree | 96abdce0ce13a2bf567a75bb0fcb40d27917c7a6 /backend/CSE2.v | |
| parent | e88c7fa00a5174ecf897b3cb59b7adee818a1788 (diff) | |
| download | compcert-kvx-b55e522ca286bbe96be3ce5fc05c984b2a4a130a.tar.gz compcert-kvx-b55e522ca286bbe96be3ce5fc05c984b2a4a130a.zip | |
invariant guaranteed
Diffstat (limited to 'backend/CSE2.v')
| -rw-r--r-- | backend/CSE2.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/CSE2.v b/backend/CSE2.v index 2fc0c323..a818996b 100644 --- a/backend/CSE2.v +++ b/backend/CSE2.v @@ -268,6 +268,8 @@ Module ADD_BOTTOM(L : SEMILATTICE_WITHOUT_BOTTOM). - apply L.ge_refl. apply L.eq_refl. Qed. + + Definition top := Some RELATION.top. End ADD_BOTTOM. Module RB := ADD_BOTTOM(RELATION). @@ -441,7 +443,7 @@ Definition apply_instr' code (pc : node) (ro : RB.t) : RB.t := Definition forward_map (f : RTL.function) := DS.fixpoint (RTL.fn_code f) RTL.successors_instr - (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) (Some RELATION.top). + (apply_instr' (RTL.fn_code f)) (RTL.fn_entrypoint f) RB.top. Definition forward_move_b (rb : RB.t) (x : reg) := match rb with |