From 26429b3ef0ca3fe91b4235ba4eae5f8b94c47357 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 19 Apr 2024 16:06:25 +0200
Subject: [PATCH] [tests] add various tests for incorrect VLA declarations
---
tests/syntax/array_size.c | 39 +++++++++++++++++++++
tests/syntax/array_size.i | 7 ----
tests/syntax/oracle/array_size.0.res.oracle | 5 +++
tests/syntax/oracle/array_size.1.res.oracle | 6 ++++
tests/syntax/oracle/array_size.2.res.oracle | 12 +++++++
tests/syntax/oracle/array_size.3.res.oracle | 6 ++++
tests/syntax/oracle/array_size.4.res.oracle | 6 ++++
tests/syntax/oracle/array_size.5.res.oracle | 6 ++++
tests/syntax/oracle/array_size.res.oracle | 4 ---
9 files changed, 80 insertions(+), 11 deletions(-)
create mode 100644 tests/syntax/array_size.c
delete mode 100644 tests/syntax/array_size.i
create mode 100644 tests/syntax/oracle/array_size.0.res.oracle
create mode 100644 tests/syntax/oracle/array_size.1.res.oracle
create mode 100644 tests/syntax/oracle/array_size.2.res.oracle
create mode 100644 tests/syntax/oracle/array_size.3.res.oracle
create mode 100644 tests/syntax/oracle/array_size.4.res.oracle
create mode 100644 tests/syntax/oracle/array_size.5.res.oracle
delete mode 100644 tests/syntax/oracle/array_size.res.oracle
diff --git a/tests/syntax/array_size.c b/tests/syntax/array_size.c
new file mode 100644
index 00000000000..53e28e8755b
--- /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 e8d46d0178a..00000000000
--- 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 00000000000..fea23a0a093
--- /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 00000000000..2cc9bdd172a
--- /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 00000000000..68a2e549d6b
--- /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 00000000000..4eab8e1413c
--- /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 00000000000..3e0926c04d6
--- /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 00000000000..d308118b0fb
--- /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 ea94c308541..00000000000
--- 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.
--
GitLab