Refactor Theta Cfa generation

ftsrg · Feb 7, 2021 · 453d2e0 · 453d2e0
1 parent da5fcf9
commit 453d2e0
Show file tree

Hide file tree

Showing 11 changed files with 515 additions and 398 deletions.
diff --git a/test/theta/cfa/Expected/counter.theta b/test/theta/cfa/Expected/counter.theta
@@ -1,6 +1,6 @@
 main process __gazer_main_process {
     var main_RET_VAL : int
-    var main_tmp : int
+    var main_call : int
     var main___gazer_error_field : int
     init loc loc0
     final loc loc1
@@ -15,15 +15,15 @@ main process __gazer_main_process {
     }
 
     loc2 -> loc3 {
-        havoc main_tmp
+        havoc main_call
     }
 
     loc3 -> loc6 {
-        assume (not (1 <= main_tmp))
+        assume (not (1 <= main_call))
     }
 
     loc3 -> loc4 {
-        assume (not (not (1 <= main_tmp)))
+        assume (not (not (1 <= main_call)))
     }
 
     loc4 -> loc5 {
@@ -44,4 +44,4 @@ main process __gazer_main_process {
         main___gazer_error_field := 2
     }
 
-}
+}
diff --git a/test/theta/cfa/Output/counter.c.tmp b/test/theta/cfa/Output/counter.c.tmp
diff --git a/tools/gazer-theta/CMakeLists.txt b/tools/gazer-theta/CMakeLists.txt
@@ -2,7 +2,9 @@ set(LIB_SOURCE_FILES
     lib/ThetaCfaGenerator.cpp
     lib/ThetaExpr.cpp
     lib/ThetaVerifier.cpp
-    lib/ThetaCfaWriterPass.cpp)
+    lib/ThetaCfaWriterPass.cpp
+    lib/ThetaCfaProcedureGenerator.cpp
+    lib/ThetaCommon.cpp)
 
 set(TOOL_SOURCE_FILES
     gazer-theta.cpp