Two new failing tests demonstrating updates outside member bounds

These examples write to a member different from the access path being
used, yet within the object bounds.

Author: tautschnig

regression/cbmc/member_bounds1/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+
+#pragma pack(push, 1)
+struct S
+{
+  int a[2];
+  int x;
+};
+#pragma pack(pop)
+
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#endif
+
+int main()
+{
+  int A[3];
+  _Static_assert(sizeof(A) == sizeof(struct S), "");
+  struct S *s = A;
+  s->a[2] = 42;
+  assert(*((int *)s + 2) == 42);
+  assert(s->x == 42);
+  assert(A[2] == 42);
+}

regression/cbmc/member_bounds1/test.desc

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+--no-simplify
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test passes when using the simplifier, but results in "WITH" expressions
+that update elements outside their bounds without the simplifier.

regression/cbmc/member_bounds2/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+#pragma pack(push, 1)
+struct SU
+{
+  union {
+    int a[2];
+  } u;
+  int x;
+};
+#pragma pack(pop)
+
+int main()
+{
+  struct SU su;
+  su.u.a[2] = 42;
+  assert(*((int *)&su + 2) == 42);
+  assert(su.x == 42);
+}

regression/cbmc/member_bounds2/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Field sensitivity makes it (currently) impossible to update bytes outside the
+particular field. One possible way to address this is rewriting subscripted
+array accesses to pointer dereferencing, as the C standard describes. Here, this
+would amount to using *(&su.u.a[0] + 2) instead of su.u.a[2].