diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 18:21:46 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-05 18:21:46 +0100 |
| commit | 5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f (patch) | |
| tree | 1e74a15034fe762df2b44289b1cb7d1ccac31a99 | |
| parent | 746b4cd3895462be7959389ef39696294177e465 (diff) | |
| download | compcert-kvx-5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f.tar.gz compcert-kvx-5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f.zip | |
just the analysis
| -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 |