From 123074c38671e76dbf8678a5f116970ab2f5a799 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 9 Jan 2020 06:41:49 +0100 Subject: fix bug in xfer function --- backend/ForwardMoves.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'backend/ForwardMoves.v') diff --git a/backend/ForwardMoves.v b/backend/ForwardMoves.v index 65d66b16..0e71b6b5 100644 --- a/backend/ForwardMoves.v +++ b/backend/ForwardMoves.v @@ -231,7 +231,8 @@ Module RB := ADD_BOTTOM(RELATION). Module DS := Dataflow_Solver(RB)(NodeSetForward). Definition kill (dst : reg) (rel : RELATION.t) := - PTree.remove dst rel. + PTree.filter1 (fun x => if Pos.eq_dec dst x then false else true) + (PTree.remove dst rel). Definition move (src dst : reg) (rel : RELATION.t) := PTree.set dst (match PTree.get src rel with -- cgit