Loop invariant contract havocs a pointer instead of havocing its value

[SaswatPadhi]

CBMC version: develop

Operating system: Mac OS 10.15.7

Test case:

#include <assert.h>

void main()
{
  char *data = malloc(1);
  *data = 42;

  unsigned i;
  while(i > 0)
    __CPROVER_loop_invariant(*data == 42)
    {
      *data = 42;
      i--;
    }

  assert(*data = 42);
}

Exact command line resulting in the issue:

goto-cc -o test.gb test.c
goto-instrument --enforce-all-contracts test.gb test-loop.gb
cbmc --pointer-check test-loop.gb

What behaviour did you expect:

CBMC should be able to verify the goto program with the loop contracts properly enforced.

What happened instead:

CBMC complains that data is assigned to NULL and thus *data = 42 may be invalid.

This happens because the __CPROVER_loop_invariant contract incorrectly havocs the write set of the loop -- instead of havocing *data, it havocs data and non-deterministically sets it to NULL.

[SaswatPadhi]

cc: @feliperodri @markrtuttle