Extend the previous test with an access to the array

The test currently fails an invariant in the array decision procedure.

Author: tautschnig

regression/cbmc/vla2/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+
+int main(int argc, char *argv[])
+{
+  unsigned char x = argc;
+  // make sure int multiplication below won't overflow - type casting to
+  // unsigned long long would be possible, but puts yields a challenging problem
+  // for the SAT solver
+  __CPROVER_assume(x < 1ULL << (sizeof(int) * 8 / 2 - 1));
+
+  struct S
+  {
+    int a;
+    int b[x];
+    int c;
+  };
+
+  if(x % 2 == 0)
+    x = 3;
+
+  struct S s[x];
+
+  if((unsigned char)argc > 0)
+  {
+    s[0].b[0] = 42;
+    assert(s[0].b[0] == 42);
+  }
+
+  __CPROVER_assume(x < 255);
+  ++x;
+
+  assert(sizeof(struct S) == ((unsigned char)argc + 2) * sizeof(int));
+  assert(sizeof(s) == (x - 1) * ((unsigned char)argc + 2) * sizeof(int));
+
+  return 0;
+}

regression/cbmc/vla2/test.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The array decision procedure does not yet handle member expressions.