Skip to content

Commit ef7a4df

Browse files
committed
pointer encoding: tests changed
1 parent 5b9c00b commit ef7a4df

File tree

6 files changed

+6
-6
lines changed

6 files changed

+6
-6
lines changed

regression/cbmc-library/fprintf-01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

regression/cbmc-library/free-01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--pointer-check --bounds-check --stop-on-fail
4-
free argument must be NULL or valid pointer
4+
free argument must be (dynamic object|NULL or valid pointer)
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$

regression/cbmc/address_space_size_limit1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE thorough-paths broken-smt-backend
1+
KNOWNBUG thorough-paths broken-smt-backend
22
test.c
33
--no-simplify --unwind 300 --object-bits 8
44
too many addressed objects

regression/cbmc/memory_allocation1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE broken-smt-backend
1+
KNOWNBUG broken-smt-backend
22
main.c
33
--pointer-check
44
^EXIT=10$

regression/cbmc/mm_io1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33

44
^EXIT=0$

regression/cbmc/pointer-extra-checks/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
KNOWNBUG
22
main.c
33
--pointer-check
44
^EXIT=10$

0 commit comments

Comments
 (0)