Skip to content

Commit 9c60ccd

Browse files
committed
Add tests of new command line option
So that the new option has some basic tests and a directory to place tests for follow-up functionality. Note that all tests are currently passed the `--slice-formula` argument so that unimplemented functionality from `__cprover_initialise` does not get passed to the solver if the user code does not depend on it. This will support incremental implementation of each slice of work in doing the implementation. Once the implementation is sufficiently complete to support all expressions generated from `__cprover_initialise`, the `--slice-formula` argument can be removed again.
1 parent bf69ae6 commit 9c60ccd

File tree

6 files changed

+38
-0
lines changed

6 files changed

+38
-0
lines changed

regression/CMakeLists.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@ add_subdirectory(cpp)
3232
add_subdirectory(cbmc-concurrency)
3333
add_subdirectory(cbmc-cover)
3434
add_subdirectory(cbmc-incr-oneloop)
35+
add_subdirectory(cbmc-incr-smt2)
3536
add_subdirectory(cbmc-incr)
3637
add_subdirectory(cbmc-with-incr)
3738
add_subdirectory(array-refinement-with-incr)

regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ DIRS = cbmc \
1010
cbmc-concurrency \
1111
cbmc-cover \
1212
cbmc-incr-oneloop \
13+
cbmc-incr-smt2 \
1314
cbmc-incr \
1415
cbmc-with-incr \
1516
array-refinement-with-incr \
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
2+
add_test_pl_tests(
3+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula"
4+
)

regression/cbmc-incr-smt2/Makefile

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
default: test
2+
3+
include ../../src/config.inc
4+
include ../../src/common
5+
6+
test:
7+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula"
8+
9+
tests.log: ../test.pl test
10+
11+
clean:
12+
find . -name '*.out' -execdir $(RM) '{}' \;
13+
find . -name '*.smt2' -execdir $(RM) '{}' \;
14+
$(RM) tests*.log
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
test.c
3+
--incremental-smt2-solver z3
4+
Passing problem to incremental SMT2 solving via "z3"
5+
^EXIT=(0|127|134|137)$
6+
^SIGNAL=0$
7+
--
8+
--
9+
Test that running cbmc with the `--incremental-smt2-solver` argument causes the
10+
incremental smt2 solving to be used. Note that at the time of adding this test,
11+
an invariant violation is expected due to the unimplemented solving.
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
2+
int main()
3+
{
4+
int x;
5+
__CPROVER_assert(x, "Nondeterministic int assert.");
6+
return 0;
7+
}

0 commit comments

Comments
 (0)