Member expression bounds checking in multiple assignments

[kkjeer]

This PR fixes an issue with bounds checking member expressions across multiple assignments.

Consider an example:

struct S {
  int len;
  _Array_ptr<int> p : count(len);
};

void f(struct S *s, _Array_ptr<int> arr : count(3)) {
  s->p = arr, s->len = 3;
}

After the assignment s->p = arr, the observed bounds of s->p are bounds(arr, arr + 3). At the assignment s->len = 3, we synthesize the member expression s->p whose target bounds bounds(s->p, s->p + s->len) use the value of s->len. However, since s->p already has observed bounds recorded in State.ObservedBounds, we do not update the observed bounds of s->p to its target bounds. Therefore, the assignment to s->len does not modify the observed bounds of s->p. At the end of this statement, the observed bounds of s->p are bounds(arr, arr + 3) and we have equality between s->p and arr and between s->len and 3. The observed bounds bounds(arr, arr + 3) imply the target bounds bounds(s->p, s->p + s->len). No errors or warnings are emitted.

[sulekhark]

LGTM! Thank you!

[kkjeer]

TODO: at the assignment s->a++, the observed bounds of the RHS s->a + 1 of the assignment should be bounds(s->b, s->b + 2), not bounds(s->a, s->a + 2). This can be done in a follow-up PR.