[tests] add various tests for incorrect VLA declarations

tests/syntax/array_size.c

+/* run.config*
+ EXIT: 1
+   OPT: -cpp-extra-args="-DNEG_SIZE"
+   OPT: -cpp-extra-args="-DVLA_INIT1"
+   OPT: -cpp-extra-args="-DVLA_INIT2"
+   OPT: -cpp-extra-args="-DVLA_GLOB1"
+   OPT: -cpp-extra-args="-DVLA_GLOB2"
+   OPT: -cpp-extra-args="-DVLA_STRUCT"
+*/
+
+#ifdef NEG_SIZE
+int f(int t[-1]) { return t[0]; } // should raise an error
+#endif
+
+#ifdef VLA_INIT1
+void g(int size) {
+  int a[size] = { 0 }; // error: VLA can't be initialized
+}
+#endif
+
+#ifdef VLA_INIT2
+void h (int size) {
+  int a [2][size] = { { 0 } }; // same as above
+}
+#endif
+
+const int size = 42;
+
+#ifdef VLA_GLOB1
+int a[size]; // error: global arrays must have a fixed size.
+#endif
+
+#ifdef VLA_GLOB2
+int a[2][size]; // same as above
+#endif
+
+#ifdef VLA_STRUCT
+struct { int a [size]; }; // error: no VLA in struct
+#endif

tests/syntax/array_size.i

-/* run.config*
- EXIT: 1
-   STDOPT:
-*/
-
-
-int f(int t[-1]) { return t[0]; } // should raise an error

tests/syntax/oracle/array_size.0.res.oracle

+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:12: User Error: Array length is negative.
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+  for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/array_size.1.res.oracle

+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:17: User Error: 
+  Variable-sized array cannot have initializer
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+  for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/array_size.2.res.oracle

+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:23: User Error: 
+  "Variable length array in structure" extension is not supported
+[kernel] array_size.c:23: User Error: 
+  Array length size is not a compile-time constant: no explicit initializer allowed.
+  21    #ifdef VLA_INIT2
+  22    void h (int size) {
+  23      int a [2][size] = { { 0 } }; // same as above
+                    ^^^^
+  24    }
+  25    #endif
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/array_size.3.res.oracle

+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:30: User Error: 
+  "Variable length array in structure" extension is not supported
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+  for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/array_size.4.res.oracle

+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:34: User Error: 
+  "Variable length array in structure" extension is not supported
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+  for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/array_size.5.res.oracle

+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:38: User Error: 
+  "Variable length array in structure" extension is not supported
+[kernel] User Error: stopping on file "array_size.c" that has errors. Add '-kernel-msg-key pp'
+  for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/array_size.res.oracle

-[kernel] Parsing array_size.i (no preprocessing)
-[kernel] array_size.i:7: User Error: Array length is negative.
-[kernel] User Error: stopping on file "array_size.i" that has errors.
-[kernel] Frama-C aborted: invalid user input.