Closed
Description
CBMC version: 99f1a2e
Operating system: 10.15.7
Test case:
#include <assert.h>
#include <stdlib.h>
#define SIZE 8
struct blob { char *data; };
void main()
{
struct blob *b = malloc(sizeof(struct blob));
b->data = malloc(SIZE);
b->data[5] = 0;
for (unsigned i = 0; i < SIZE; i++)
__CPROVER_loop_invariant(i <= SIZE)
{
b->data[i] = 1;
}
assert(b->data[5] == 0);
}Exact command line resulting in the issue:
$ goto-cc test.c -o test.1.gb
$ goto-instrument --enforce-all-contracts test.1.gb test.2.gbWhat behaviour did you expect:
goto-instrument would decompose the invariant contract to appropriate assertions and assumptions.
What happened instead:
goto-instrument crashes with a precondition violation:
$ goto-instrument --enforce-all-contracts test.1.gb test.2.gb
Reading GOTO program from 'test2.goto'
--- begin invariant violation report ---
Invariant check failed
File: ../util/pointer_expr.h:387 function: dereference_exprt
Condition: op.type().id() == ID_pointer
Reason: Precondition
Backtrace:
...Additional Information:
In this case local_may_alias.get is imprecise and returns an unknown expression for the pointer being modified (b->data[i]).
We should avoid the crash and show a warning / error regarding the imprecision of the alias analysis.