Description
CBMC version: 5.94.0
Operating system: macOS 13.5.2
Exact command line resulting in the issue:
goto-cc main.c
goto-instrument --pointer-check a.out b.out
goto-instrument --apply-loop-contracts b.out c.out
cbmc c.out
What behaviour did you expect: SUCCESS
What happened instead:
...
[main.3] line 9 Check that loop invariant is preserved: FAILURE
...
[main.pointer_dereference.11] line 14 dereference failure: pointer outside object bounds in *tmp_post_array: FAILURE
In the following program, we malloc a nondeterministic array array and compute the sum s of the elements of array with a loop. The loop contracts guarantees that the offset of array never exceeds the object size of array, so that the dereference in the loop body should not fail the pointer checks.
void main()
{
unsigned short len;
__CPROVER_assume(len >= 8);
char *array = malloc(len);
const char *end = array + len;
unsigned s = 0;
while(array != end)
__CPROVER_loop_invariant(
__CPROVER_same_object(array, end) &&
__CPROVER_POINTER_OFFSET(array) <= __CPROVER_OBJECT_SIZE(array))
{
s += *array++;
}
}However, the trace shows that the actual malloc size (36028797018963967ul) is not the size 65535 we pass to the malloc function. Note that the last two bytes of them are consistent. So the issue could be that the unspecified bits are set nondeterministic.
State 12 file main.c function main line 3 thread 0
----------------------------------------------------
len=65535 (11111111 11111111)
Assumption:
file main.c line 4 function main
(signed int)len >= 8
State 18 file main.c function main line 5 thread 0
----------------------------------------------------
malloc_size=36028797018963967ul (00000000 01111111 11111111 11111111 11111111 11111111 11111111 11111111)
State 21 file <builtin-library-malloc> function malloc line 42 thread 0
----------------------------------------------------
malloc_res=NULL (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000000)
State 23 file <builtin-library-malloc> function malloc line 43 thread 0
----------------------------------------------------
dynamic_object_size=36028797018963967ul (00000000 01111111 11111111 11111111 11111111 11111111 11111111 11111111)
The issue is resolved once I change the type of len from unsigned short to unsigned long