From 14388a6be6cf7aac50f2af4ff29fe9726ad83435 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 21 Apr 2020 18:04:43 +0200
Subject: improvement in precision

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

(limited to 'backend/CSE3analysis.v')

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index d3d1c043..b495371d 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -64,6 +64,7 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
   Qed.
   
   Definition lub := PSet.inter.
+  Definition glb := PSet.union.
   
   Lemma ge_lub_left: forall x y, ge (lub x y) x.
   Proof.
@@ -274,7 +275,8 @@ Section OPERATIONS.
   Definition oper (dst : reg) (op: sym_op) (args : list reg)
              (rel : RELATION.t) : RELATION.t :=
     match rhs_find op (forward_move_l rel args) rel with
-    | Some r => move r dst rel
+    | Some r => RELATION.glb (move r dst rel)
+                             (oper1 dst op args rel)
     | None => oper1 dst op args rel
     end.
   
-- 
cgit