diff options
Diffstat (limited to 'backend/Allocation.v')
| -rw-r--r-- | backend/Allocation.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index c66d6b0..74c85cf 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -3,6 +3,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Lattice. Require Import AST. Require Import Integers. Require Import Values. @@ -100,7 +101,8 @@ Definition transfer general framework for backward dataflow analysis provided by module [Kildall]. *) -Module DS := Backward_Dataflow_Solver(Regset)(NodeSetBackward). +Module RegsetLat := LFSet(Regset). +Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward). Definition analyze (f: RTL.function): option (PMap.t Regset.t) := DS.fixpoint (successors f) f.(fn_nextpc) (transfer f) nil. |