Skip to content

Commit 1a0b3ee

Browse files
author
Remi Delmas
committed
Add failures due to CAR size overflow in is_fresh
1 parent 7bdf6f7 commit 1a0b3ee

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE dfcc-only
22
main.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$

0 commit comments

Comments
 (0)