Skip to content

Commit b2fe035

Browse files
smowtonsmowton
committed
JBMC: enable SSA equation validation in all regression tests
1 parent d53bf4b commit b2fe035

File tree

12 files changed

+38
-38
lines changed

12 files changed

+38
-38
lines changed

‎jbmc/regression/jbmc-concurrency/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc> --validate-goto-model"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)

‎jbmc/regression/jbmc-concurrency/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
9+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/jbmc-generics/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc> --validate-goto-model"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"jbmc-generics-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --validate-goto-model --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc-generics/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
1212

1313
show:
1414
@for dir in *; do \

‎jbmc/regression/jbmc-inheritance/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc> --validate-goto-model"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)

‎jbmc/regression/jbmc-inheritance/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
77

88
tests.log: ../$(CPROVER_DIR)/regression/test.pl
9-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
9+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
1010

1111
show:
1212
@for dir in *; do \

‎jbmc/regression/jbmc-strings/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc> --validate-goto-model"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"jbmc-strings-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --validate-goto-model --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc-strings/Makefile

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
testfuture:
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
1212

1313
testall:
14-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
14+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
18-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
18+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
2020

2121
show:
2222
@for dir in *; do \

‎jbmc/regression/jbmc/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc> --validate-goto-model"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"jbmc-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --validate-goto-model --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc/Makefile

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,12 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
1212

1313
show:
1414
@for dir in *; do \

‎jbmc/regression/strings-smoke-tests/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:jbmc> --validate-goto-model"
2+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
33
)
44

55
add_test_pl_profile(
66
"strings-smoke-tests-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --validate-goto-model --symex-driven-lazy-loading"
7+
"$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
88
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/strings-smoke-tests/Makefile

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,20 @@ default: tests.log
33
include ../../src/config.inc
44

55
test:
6-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
6+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
testfuture:
10-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
10+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CF
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
1212

1313
testall:
14-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model" -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
14+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" -CFTK
15+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
18-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model"
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
18+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation"
19+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
2020

2121
show:
2222
@for dir in *; do \

0 commit comments

Comments
 (0)