diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 06:41:49 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 06:41:49 +0100 |
| commit | 123074c38671e76dbf8678a5f116970ab2f5a799 (patch) | |
| tree | eb16c445a4d095eafbfd2dcb24a7f4c424e1a173 /backend/ForwardMoves.v | |
| parent | fd24564480c438da9456d781ec17bfa3ac6277c1 (diff) | |
| download | compcert-kvx-123074c38671e76dbf8678a5f116970ab2f5a799.tar.gz compcert-kvx-123074c38671e76dbf8678a5f116970ab2f5a799.zip | |
fix bug in xfer function
Diffstat (limited to 'backend/ForwardMoves.v')
| -rw-r--r-- | backend/ForwardMoves.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 |