issues with auto-objects

[remi-delmas-3000]

Below are a couple of issues encountered when trying to use auto objects.

In this one the last assertion fails, but it passes if we replace the rw_ok assumptions with explicit mallocs for both pointers. Pointer checks pass on this model

#include <assert.h>
#include <stdlib.h>
// run with cbmc --pointer-check --bounds-check
int main() {
  size_t n = 3;

  unsigned int *a;
  __CPROVER_assume(__CPROVER_rw_ok(a, n * sizeof(*a)));
  assert(a);

  unsigned int *old_a;
  __CPROVER_assume(__CPROVER_rw_ok(old_a, n * sizeof(*old_a)));
  assert(old_a);

  __CPROVER_array_copy(old_a, a);
  assert(__CPROVER_array_equal(old_a, a));

  for (size_t i = 0; i < n; i++) {
    a[i] += 1;
  }

  assert(__CPROVER_forall {
    size_t i;
    i<n ==> a[i] == (old_a[i] + 1)
  });
}

In this one, accessing an auto object through aliases fails pointer checks, both for aliases created before and created after emitting the assumption that summons the auto object. Strangely enough program assertions that depend on these dereferences pass.

#include <assert.h>
#include <stdlib.h>

// tries to answer the question: do auto-object assumptions propagate to
// aliases created before the assumption is emitted ?
// run with cbmc --pointer-check --bounds-check
int main() {
  unsigned int *a;
  unsigned int *b;
  unsigned int *c;

  // create alias before assumption
  b = a;
  __CPROVER_assume(__CPROVER_rw_ok(a, sizeof(*a)));

  // create alias after assumption
  c = a;

  assert(a);
  assert(b);
  assert(c);

  // dereference fails for both b and c with --pointer-check
  assert(*b == *a);
  assert(*c == *a);

  *a = 1;
  // assertions pass but --pointer-checks fail
  assert(*b == 1);
  assert(*c == 1);
}

CBMC version: 5.88.1
Operating system: macOS
Exact command line resulting in the issue: c
What behaviour did you expect:
What happened instead: