diff options
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | backend/CSE3analysis.v (renamed from backend/CSE3.v) | 3 | ||||
-rw-r--r-- | extraction/extraction.v | 4 |
3 files changed, 6 insertions, 3 deletions
@@ -89,7 +89,7 @@ BACKEND=\ CSEdomain.v CombineOp.v CSE.v CombineOpproof.v CSEproof.v \ CSE2deps.v CSE2depsproof.v \ CSE2.v CSE2proof.v \ - CSE3.v \ + CSE3analysis.v \ NeedDomain.v NeedOp.v Deadcode.v Deadcodeproof.v \ Unusedglob.v Unusedglobproof.v \ Machregs.v Locations.v Conventions1.v Conventions.v LTL.v \ diff --git a/backend/CSE3.v b/backend/CSE3analysis.v index 0ac56b36..06de1b08 100644 --- a/backend/CSE3.v +++ b/backend/CSE3analysis.v @@ -75,4 +75,7 @@ Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM. Qed. End RELATION. +Module RB := ADD_BOTTOM(RELATION). +Module DS := Dataflow_Solver(RB)(NodeSetForward). + Definition totoro := RELATION.lub. diff --git a/extraction/extraction.v b/extraction/extraction.v index a258d4d8..ea30e7c2 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -36,7 +36,7 @@ Require Parser. Require Initializers. Require Asmaux. -Require CSE3. (* FIXME *) +Require CSE3analysis. (* FIXME *) (* Standard lib *) Require Import ExtrOcamlBasic. @@ -188,7 +188,7 @@ Set Extraction AccessOpaque. Cd "extraction". Separate Extraction - CSE3.totoro (* FIXME *) + CSE3analysis.totoro (* FIXME *) Compiler.transf_c_program Compiler.transf_cminor_program Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env |