1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
CORE dfcc-only
main.c
--malloc-may-fail --malloc-fail-assert --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh max allocation size exceeded: FAILURE$
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?0\] is assignable: SUCCESS$
^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\(size - \(.*\)1\)\] is assignable: SUCCESS$
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(.*\))?\(size - \(.*\)1\)\]: SUCCESS$
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
--
--
This tests shows that using is_fresh with --malloc-fail-assert active and
without imposing a limit on the size parameter results in an failed assertion
in is_fresh that detects that the size may be too large, but also results in an
implicit assumption that the size is less than the maximum allocation size
(just like when used with malloc).
|
