We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 1a0b3ee commit 79d3ca8Copy full SHA for 79d3ca8
regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc
@@ -1,9 +1,8 @@
1
CORE dfcc-only
2
main.c
3
--no-malloc-may-fail --dfcc main --enforce-contract foo
4
+^\[__CPROVER_contracts_car_create.assertion.d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
5
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
-^\[__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$
7
^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
8
^EXIT=10$
9
^SIGNAL=0$
0 commit comments