Crash in enforcing loop invariant contract due to imprecise alias analysis

[SaswatPadhi]

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.gb

What 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.

[SaswatPadhi]

Based on discussions with @tautschnig and @mww-aws:

• we should allow __CPROVER_assigns annotations on loops
• we should show an error in this case and instruct the user to use __CPROVER_assigns since automatic inference of the modified set was imprecise

[SaswatPadhi]

Removed the pending merge label.

The commit that referred to this issue added some KNOWNBUG regression tests that should pass once this issue is resolved. The commit does not fix this issue. Sorry if that was confusing.