1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
CORE dfcc-only
main.c
--dfcc main --replace-call-with-contract foo
^\[bar.assertion.\d+\] line 33 assertion 0: FAILURE$
^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
^\[bar.assertion.\d+\] line 39 assertion 0: FAILURE$
^\[bar.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$
^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts.
The postcondition of `foo` describes a disjunction of cases: either `x` equals `a` and `y` is null,
or `x` is null and `y` equals `a`. The function `bar` branches on `y == NULL`.
The test succeeds if the two `assert(0)` are falsifiable, which which shows that
both cases of the disjunction expressed in the ensures clause of `foo` are reachable.
|
