Skip to content

Commit 4d8743f

Browse files
esteffinEnrico Steffinlongo
authored and
Enrico Steffinlongo
committed
Fixed contract-dfcc failing regression test
1 parent 34d005d commit 4d8743f

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Diff for: regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE dfcc-only
22
main.c
3-
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
3+
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check --no-standard-checks
44
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
55
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
66
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$

0 commit comments

Comments
 (0)