Skip to content

Commit 2864842

Browse files
committed
Memory predicates test: avoid undefined behaviour
There already is an assertion in place to guard against undefined behaviour. We shouldn't have to match on particular outcomes of undefined behaviour that occurs after that assertion.
1 parent fb65095 commit 2864842

File tree

2 files changed

+2
-8
lines changed

2 files changed

+2
-8
lines changed

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ __CPROVER_assigns(__CPROVER_object_from(arr))
88
{
99
__CPROVER_assert(arr != NULL, "arr is not NULL");
1010
__CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped");
11-
if(size > 0)
11+
if(size > 0 && size < __CPROVER_max_malloc_size)
1212
{
1313
arr[0] = 0;
1414
arr[size - 1] = 0;

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

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,8 @@ CORE
22
main.c
33
--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
44
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
5-
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
6-
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
75
^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
8-
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: FAILURE$
9-
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: FAILURE$
10-
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
11-
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
12-
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: FAILURE$
6+
^\*\* 2 of \d+ failed
137
^EXIT=10$
148
^SIGNAL=0$
159
^VERIFICATION FAILED$

0 commit comments

Comments
 (0)