File tree Expand file tree Collapse file tree 15 files changed +26
-16
lines changed
regression/cbmc-incr-smt2
bitvector-arithmetic-operators
bitvector-bitwise-operators
nondeterministic-int-assert Expand file tree Collapse file tree 15 files changed +26
-16
lines changed Original file line number Diff line number Diff line change 5
5
set (exclude_win_broken_tests "" )
6
6
endif ()
7
7
8
- add_test_pl_tests (
9
- "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests}
8
+ add_test_pl_profile (
9
+ "cbmc-new-smt-backend-z3"
10
+ "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula ${exclude_win_broken_tests} "
11
+ "-C;-s;new-smt-z3"
12
+ "CORE"
13
+ )
14
+
15
+ add_test_pl_profile (
16
+ "cbmc-new-smt-backend-cv4"
17
+ "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc4 --lang smt' --validate-goto-model --validate-ssa-equation --slice-formula ${exclude_win_broken_tests} "
18
+ "-C;-s;new-smt-cvc4"
19
+ "CORE"
10
20
)
Original file line number Diff line number Diff line change 1
1
CORE
2
2
overflow_behaviour.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- trace
3
+ --trace
4
4
\[main\.assertion\.1\] line \d+ Wrap-around to INT_MIN when adding to INT_MAX: SUCCESS
5
5
\[main\.assertion\.2\] line \d+ Wrap-around to INT_MAX when subtracting from INT_MIN: SUCCESS
6
6
\[main\.assertion\.3\] line \d+ INT_MAX minus INT_MIN equals -1: SUCCESS
Original file line number Diff line number Diff line change 1
1
CORE
2
2
polynomial.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- trace
3
+ --trace
4
4
\[main\.assertion\.1\] line \d+ No negative solution: FAILURE
5
5
\[main\.assertion\.2\] line \d+ No positive solution: FAILURE
6
6
x=-8\ \(11111111 11111111 11111111 11111000\)
Original file line number Diff line number Diff line change 1
1
CORE
2
2
simple_equation.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- trace --verbosity 10
3
+ --trace --verbosity 10
4
4
\[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
5
5
\[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
6
6
\[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS
Original file line number Diff line number Diff line change 1
1
CORE
2
2
unsigned_behaviour.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- trace
3
+ --trace
4
4
\[main\.assertion\.1\] line \d+ a plus b should be more than 27: FAILURE
5
5
\[main\.assertion\.2\] line \d+ a plus b should be more than 27: FAILURE
6
6
\[main\.assertion\.3\] line \d+ c plus d should be more than 27: FAILURE
Original file line number Diff line number Diff line change 1
1
CORE
2
2
bitwise_ops.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- slice-formula
3
+ --slice-formula
4
4
\[main\.assertion\.1\] line \d+ This is going to fail for bit-opposites: FAILURE
5
5
\[main\.assertion\.2\] line \d+ This is going to hold for all values != 0: SUCCESS
6
6
\[main\.assertion\.3\] line \d+ This is going to fail for the same value in A and B: FAILURE
Original file line number Diff line number Diff line change 1
1
CORE
2
2
shift_left.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- slice-formula
3
+ --slice-formula
4
4
\[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE
5
5
^EXIT=10$
6
6
^SIGNAL=0$
Original file line number Diff line number Diff line change 1
1
CORE
2
2
shift_right.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- slice-formula --trace
3
+ --slice-formula --trace
4
4
\[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
5
5
\[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
6
6
\[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
Original file line number Diff line number Diff line change 1
1
CORE
2
2
div_by_zero.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- div-by-zero-check --trace
3
+ --div-by-zero-check --trace
4
4
\[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
5
5
\[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
6
6
y=0
Original file line number Diff line number Diff line change 1
1
KNOWNBUG
2
2
signed_overflow.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- signed-overflow-check --trace
3
+ --signed-overflow-check --trace
4
4
^VERIFICATION FAILED$
5
5
^EXIT=10$
6
6
^SIGNAL=0$
Original file line number Diff line number Diff line change 1
1
CORE
2
2
control_flow.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- verbosity 10
3
+ --verbosity 10
4
4
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5
5
Sending command to SMT2 solver - \(set-option :produce-models true\)
6
6
Sending command to SMT2 solver - \(set-logic QF_UFBV\)
Original file line number Diff line number Diff line change 1
1
CORE
2
2
test.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- verbosity 10
3
+ --verbosity 10
4
4
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5
5
Sending command to SMT2 solver - \(set-option :produce-models true\)
6
6
Sending command to SMT2 solver - \(set-logic QF_UFBV\)
Original file line number Diff line number Diff line change 1
1
CORE
2
2
stdbool_example.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- trace
3
+ --trace
4
4
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5
5
VERIFICATION FAILED
6
6
equal=FALSE\s*\([0 ]+\)
Original file line number Diff line number Diff line change 1
1
CORE
2
2
trace.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- trace
3
+ --trace
4
4
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5
5
Assert of inequality to 4\.: FAILURE
6
6
Assert of inequality to 2\.: FAILURE
Original file line number Diff line number Diff line change 1
1
CORE
2
2
valid_unsat.c
3
- --incremental-smt2-solver 'z3 --smt2 -in' -- verbosity 10
3
+ --verbosity 10
4
4
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5
5
Sending command to SMT2 solver - \(check-sat\)
6
6
Solver response - unsat
You can’t perform that action at this time.
0 commit comments