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 /backend | |
| parent | 746b4cd3895462be7959389ef39696294177e465 (diff) | |
| download | compcert-kvx-5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f.tar.gz compcert-kvx-5e2b2d9a6c85a2ed90eda0fe630a218e8b437c5f.zip | |
just the analysis
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/CSE3analysis.v (renamed from backend/CSE3.v) | 3 |
1 files changed, 3 insertions, 0 deletions
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. |