Replace with contracts - havoc entire array content

[feliperodri]

CBMC version: develop (current 06c563a)

Operating system: N/A.

Exact command line resulting in the issue:

goto-cc *.c -o main.gb && goto-instrument main.gb main-mod.gb --replace-all-calls-with-contracts && cbmc main-mod.gb

#include <assert.h>

void foo(char c[]) __CPROVER_assigns(*c)
{
}

int main()
{
  char b[2];
  b[0] = 'a';
  b[1] = 'b';
  foo(b);
  assert(b[0] == 'a');
  assert(b[1] == 'b');
  return 0;
}

What behaviour did you expect:

** Results:
main.c function main
[main.assertion.1] line 13 assertion b[0] == 'a': FAILURE
[main.assertion.2] line 14 assertion b[1] == 'b': FAILURE

What happened instead:

** Results:
main.c function main
[main.assertion.1] line 13 assertion b[0] == 'a': FAILURE
[main.assertion.2] line 14 assertion b[1] == 'b': SUCCESS

We need to havoc all contents of an array.