diff --git a/tests/syntax/array_size.c b/tests/syntax/array_size.c new file mode 100644 index 0000000000000000000000000000000000000000..53e28e8755be8048a938d80023d5ee5b6e3e4b60 --- /dev/null +++ b/tests/syntax/array_size.c @@ -0,0 +1,39 @@ +/* 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 diff --git a/tests/syntax/array_size.i b/tests/syntax/array_size.i deleted file mode 100644 index e8d46d0178a748a46145d63601c3f5ba9b1711af..0000000000000000000000000000000000000000 --- a/tests/syntax/array_size.i +++ /dev/null @@ -1,7 +0,0 @@ -/* run.config* - EXIT: 1 - STDOPT: -*/ - - -int f(int t[-1]) { return t[0]; } // should raise an error diff --git a/tests/syntax/oracle/array_size.0.res.oracle b/tests/syntax/oracle/array_size.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..fea23a0a0938e75b5581885fc29989ef383e0b94 --- /dev/null +++ b/tests/syntax/oracle/array_size.0.res.oracle @@ -0,0 +1,5 @@ +[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. diff --git a/tests/syntax/oracle/array_size.1.res.oracle b/tests/syntax/oracle/array_size.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..2cc9bdd172ac6d1eb750d7eca455cab9eba055b9 --- /dev/null +++ b/tests/syntax/oracle/array_size.1.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/array_size.2.res.oracle b/tests/syntax/oracle/array_size.2.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..68a2e549d6bbc3abfa578fec08a2db6778ed70ad --- /dev/null +++ b/tests/syntax/oracle/array_size.2.res.oracle @@ -0,0 +1,12 @@ +[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. diff --git a/tests/syntax/oracle/array_size.3.res.oracle b/tests/syntax/oracle/array_size.3.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..4eab8e1413cc976e88ebf07b5348bc4e440a0976 --- /dev/null +++ b/tests/syntax/oracle/array_size.3.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/array_size.4.res.oracle b/tests/syntax/oracle/array_size.4.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..3e0926c04d6c03084aced5eda71a9885bd5d6f29 --- /dev/null +++ b/tests/syntax/oracle/array_size.4.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/array_size.5.res.oracle b/tests/syntax/oracle/array_size.5.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..d308118b0fb6595ecb48fe215c0be5a62fd29934 --- /dev/null +++ b/tests/syntax/oracle/array_size.5.res.oracle @@ -0,0 +1,6 @@ +[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. diff --git a/tests/syntax/oracle/array_size.res.oracle b/tests/syntax/oracle/array_size.res.oracle deleted file mode 100644 index ea94c308541ab9a6e185a5411e3df9086a762ef4..0000000000000000000000000000000000000000 --- a/tests/syntax/oracle/array_size.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[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.