Skip to content

Commit 453d2e0

Browse files
committed
Refactor Theta Cfa generation
1 parent da5fcf9 commit 453d2e0

File tree

11 files changed

+515
-398
lines changed

11 files changed

+515
-398
lines changed

test/theta/cfa/Expected/counter.theta

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
main process __gazer_main_process {
22
var main_RET_VAL : int
3-
var main_tmp : int
3+
var main_call : int
44
var main___gazer_error_field : int
55
init loc loc0
66
final loc loc1
@@ -15,15 +15,15 @@ main process __gazer_main_process {
1515
}
1616

1717
loc2 -> loc3 {
18-
havoc main_tmp
18+
havoc main_call
1919
}
2020

2121
loc3 -> loc6 {
22-
assume (not (1 <= main_tmp))
22+
assume (not (1 <= main_call))
2323
}
2424

2525
loc3 -> loc4 {
26-
assume (not (not (1 <= main_tmp)))
26+
assume (not (not (1 <= main_call)))
2727
}
2828

2929
loc4 -> loc5 {
@@ -44,4 +44,4 @@ main process __gazer_main_process {
4444
main___gazer_error_field := 2
4545
}
4646

47-
}
47+
}

test/theta/cfa/Output/counter.c.tmp

Lines changed: 0 additions & 47 deletions
This file was deleted.

tools/gazer-theta/CMakeLists.txt

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,9 @@ set(LIB_SOURCE_FILES
22
lib/ThetaCfaGenerator.cpp
33
lib/ThetaExpr.cpp
44
lib/ThetaVerifier.cpp
5-
lib/ThetaCfaWriterPass.cpp)
5+
lib/ThetaCfaWriterPass.cpp
6+
lib/ThetaCfaProcedureGenerator.cpp
7+
lib/ThetaCommon.cpp)
68

79
set(TOOL_SOURCE_FILES
810
gazer-theta.cpp

0 commit comments

Comments
 (0)