File tree Expand file tree Collapse file tree 1 file changed +3
-2
lines changed
regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes Expand file tree Collapse file tree 1 file changed +3
-2
lines changed Original file line number Diff line number Diff line change 11CORE dfcc-only
22main.c
3- --no-malloc-may-fail --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
3+ --no-malloc-may-fail --dfcc main --enforce-contract foo
44^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
5+ ^\[__CPROVER_contracts_car_create.assertion.d+\].*CAR size is less than __CPROVER_max_malloc_size: FAILURE$
6+ ^\[__CPROVER_contracts_car_set_insert.assertion.d+\].*CAR size is less than __CPROVER_max_malloc_size: FAILURE$
57^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
6- ^\*\* 2 of \d+ failed
78^EXIT=10$
89^SIGNAL=0$
910^VERIFICATION FAILED$
You can’t perform that action at this time.
0 commit comments