Skip to content

Commit 2fdec1a

Browse files
committed
Switch on existing tests fixed by adding dynamic size support
1 parent 5da3a04 commit 2fdec1a

File tree

4 files changed

+4
-4
lines changed

4 files changed

+4
-4
lines changed

regression/cbmc/Malloc11/slice-formula.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend new-smt-backend
1+
CORE new-smt-backend
22
main.c
33
--pointer-check --slice-formula
44
^EXIT=0$

regression/cbmc/Malloc11/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend new-smt-backend
1+
CORE new-smt-backend
22
main.c
33
--pointer-check
44
^EXIT=0$

regression/cbmc/pointer-predicates/at_bounds1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend new-smt-backend
1+
CORE new-smt-backend
22
at_bounds1.c
33
--pointer-primitive-check --malloc-fail-null
44
^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(q \+ (\(signed (long (long )?)?int\))?1, (\(unsigned (long (long )?)?int\))?0\): FAILURE$

regression/cbmc/simplify-array-size/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
CORE
22
main.c
33
--malloc-may-fail --malloc-fail-null
44
^VERIFICATION SUCCESSFUL$

0 commit comments

Comments
 (0)