1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
CORE dfcc-only
main_bounded.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: SUCCESS$
^\[__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=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
--
This tests shows that using is_fresh with --malloc-fail-assert active and
imposing a limit on the size parameter succeeds.
|
