From b55e522ca286bbe96be3ce5fc05c984b2a4a130a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 4 Feb 2020 17:23:41 +0100
Subject: invariant guaranteed

---
 backend/CSE2.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'backend/CSE2.v')

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
-- 
cgit