1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
CORE dfcc-only
main.c
--dfcc main --enforce-contract foo
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
the program accepts models where `__CPROVER_pointer_equals` evaluates to
false and the target pointer remains invalid.
|
