Skip to content

Commit eb8ddb4

Browse files
Merge pull request #7921 from peterschrammel/book-examples
Add ASV book CBMC examples
2 parents bf32f63 + 9581036 commit eb8ddb4

File tree

25 files changed

+383
-0
lines changed

25 files changed

+383
-0
lines changed

regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,6 +92,7 @@ add_subdirectory(cbmc-sequentialization)
9292
add_subdirectory(cpp-linter)
9393
add_subdirectory(catch-framework)
9494
add_subdirectory(libcprover-cpp)
95+
add_subdirectory(book-examples)
9596

9697
if(WITH_MEMORY_ANALYZER)
9798
add_subdirectory(snapshot-harness)

regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,7 @@ DIRS = cbmc-shadow-memory \
6363
cpp-linter \
6464
catch-framework \
6565
libcprover-cpp \
66+
book-examples \
6667
# Empty last line
6768

6869
ifeq ($(OS),Windows_NT)
Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
2+
set(gcc_only -X gcc-only)
3+
set(gcc_only_string "-X;gcc-only;")
4+
set(exclude_win_broken_tests -X winbug)
5+
# We add the string at the end of the exclusion list, so it must not
6+
# have the `;` at the end or it bugs out.
7+
set(exclude_win_broken_tests_string "-X;winbug")
8+
else()
9+
set(gcc_only "")
10+
set(gcc_only_string "")
11+
set(exclude_win_broken_tests "")
12+
set(exclude_win_broken_tests_string "")
13+
endif()
14+
15+
add_test_pl_tests(
16+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
17+
)
18+
19+
add_test_pl_profile(
20+
"cbmc-paths-lifo"
21+
"$<TARGET_FILE:cbmc> --paths lifo"
22+
"-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
23+
"CORE"
24+
)
25+
26+
add_test_pl_profile(
27+
"cbmc-cprover-smt2"
28+
"$<TARGET_FILE:cbmc> --cprover-smt2"
29+
"-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
30+
"CORE"
31+
)
32+
33+
# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
34+
add_test_pl_profile(
35+
"cbmc-new-smt-backend"
36+
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
37+
"${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
38+
"CORE"
39+
)
40+
41+
# solver appears on the PATH in Windows already
42+
if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
43+
set_property(
44+
TEST "cbmc-cprover-smt2-CORE"
45+
PROPERTY ENVIRONMENT
46+
"PATH=$ENV{PATH}:$<TARGET_FILE_DIR:smt2_solver>"
47+
)
48+
endif()

regression/book-examples/Makefile

Lines changed: 43 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,43 @@
1+
default: test
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
ifeq ($(BUILD_ENV_),MSVC)
7+
GCC_ONLY = -X gcc-only
8+
else
9+
GCC_ONLY =
10+
endif
11+
12+
test:
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
14+
15+
test-cprover-smt2:
16+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
17+
-X broken-smt-backend -X thorough-smt-backend \
18+
-X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
19+
-s cprover-smt2 $(GCC_ONLY)
20+
21+
test-z3:
22+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
23+
-X broken-smt-backend -X thorough-smt-backend \
24+
-X broken-z3-smt-backend -X thorough-z3-smt-backend \
25+
-s z3 $(GCC_ONLY)
26+
27+
test-paths-lifo:
28+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
29+
-X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
30+
-s paths-lifo $(GCC_ONLY)
31+
32+
test-new-smt-backend:
33+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
34+
-I new-smt-backend \
35+
-s new-smt-backend $(GCC_ONLY)
36+
37+
tests.log: ../test.pl test
38+
39+
clean:
40+
find . -name '*.out' -execdir $(RM) '{}' \;
41+
find . -name '*.smt2' -execdir $(RM) '{}' \;
42+
$(RM) export-symex-ready-goto/exported.symex.ready.goto
43+
$(RM) tests*.log

regression/book-examples/abs/C1.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
abs.c
3+
--function abs
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$

regression/book-examples/abs/C13.desc

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
CORE
2+
abs.c
3+
--function abs --signed-overflow-check --show-goto-functions
4+
^EXIT=0$
5+
^SIGNAL=0$

regression/book-examples/abs/C2.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
abs.c
3+
--function abs --signed-overflow-check
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$

regression/book-examples/abs/C3.desc

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
CORE
2+
abs.c
3+
--function abs --signed-overflow-check --trace
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$

regression/book-examples/abs/abs.c

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
int abs(int x)
2+
{
3+
int y = x;
4+
5+
if(x < 0)
6+
{
7+
y = -x;
8+
}
9+
10+
return y;
11+
}
Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
KNOWNBUG
2+
account.c
3+
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)