Skip to content

Commit 2ce536c

Browse files
committed
Ensure test only fails as originally designed
The test will otherwise exhibit undefined behaviour under CBMC 6 settings (where malloc may fail). This, in turn, can cause the expected patterns not to show up in the trace.
1 parent eef9677 commit 2ce536c

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

regression/cbmc/trace-values/unbounded_array.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ int main(int argc, char *argv[])
66
unsigned long size;
77
__CPROVER_assume(size < 100 && size > 10);
88
int *array = malloc(size * sizeof(int));
9+
__CPROVER_assume(array);
910
array[size - 1] = 42;
1011
int fixed_array[] = {1, 2};
1112
__CPROVER_array_replace(array, fixed_array);

0 commit comments

Comments
 (0)