Skip to content

Commit 627f70a

Browse files
committed
Test: unconstrained pointer need not be dynamic object
Depending on the model returned by the solver, the unconstrained pointer could fail one of several assertions: it need not be a dynamic object, and the test specification should accept that.
1 parent 54e2364 commit 627f70a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

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 (NULL or valid pointer|dynamic object)
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)