From 2e8e84aea389d41332ebd5a569b474d3c1de23d6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Jan 2020 20:31:41 +0100
Subject: correct semantics for bottom

---
 backend/ForwardMoves.v | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'backend/ForwardMoves.v')

diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v
index 47fd2457..96a19ecd 100644
--- a/backend/ForwardMoves.v
+++ b/backend/ForwardMoves.v
@@ -272,14 +272,16 @@ 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).
 
+Definition get_r (rel : RELATION.t) (x : reg) :=
+  match PTree.get x rel with
+  | None => x
+  | Some src => src
+  end.
+
 Definition get_rb (rb : RB.t) (x : reg) :=
   match rb with
   | None => x
-  | Some rel =>
-    match PTree.get x rel with
-    | None => x
-    | Some src => src
-    end
+  | Some rel => get_r rel x
   end.
 
 Definition subst_arg (fmap : option (PMap.t RB.t)) (pc : node) (x : reg) : reg :=
-- 
cgit