1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
CORE dfcc-only
main.c
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check --no-standard-checks
^\[__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-null active and
without imposing a limit on the size parameter results in an implicit assumption
that the size is less than the maximum allocation size
(just like malloc does, except is_fresh does not fail).
|
