1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
CORE dfcc-only
main.c
--dfcc main --replace-call-with-contract foo _ --arrays-uf-always --slice-formula
^\[__CPROVER_contracts_is_fresh.assertion.\d+] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assume context: FAILURE$
^\[__CPROVER_contracts_is_fresh.assertion.\d+] line \d+ __CPROVER_is_fresh does not conflict with other pointer predicate in assert context: FAILURE$
^\[__CPROVER_contracts_pointer_equals.assertion.\d+] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assume context: FAILURE$
^\[__CPROVER_contracts_pointer_equals.assertion.\d+] line \d+ __CPROVER_pointer_equals does not conflict with other pointer predicate in assert context: FAILURE$
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other pointer predicate in assume context: FAILURE$
^\[__CPROVER_contracts_pointer_in_range_dfcc.assertion.\d+] line \d+ __CPROVER_pointer_in_range_dfcc does not conflict with other predicate in assert context: FAILURE$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
Tests that the analysis fails when a same pointer is the target of multiple
pointer predicates at the same time.
We test all 6 pairwise combinations of is_fresh, poitner_equals,
pointer_in_range_dfcc in mode assume-requires/assert-ensures.
|
