From 91029b567d2603c42b97985c298ecd08e0013462 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Fri, 16 Apr 2021 10:15:24 +0200
Subject: [PATCH] [Cabs2cil] more explicit error message concerning multidim
VLAs
---
src/kernel_internals/typing/cabs2cil.ml | 4 ++-
tests/syntax/oracle/vla_multidim.0.res.oracle | 32 +++++++++++++++++++
tests/syntax/oracle/vla_multidim.1.res.oracle | 13 ++++++++
tests/syntax/vla_multidim.c | 19 +++++++++++
4 files changed, 67 insertions(+), 1 deletion(-)
create mode 100644 tests/syntax/oracle/vla_multidim.0.res.oracle
create mode 100644 tests/syntax/oracle/vla_multidim.1.res.oracle
create mode 100644 tests/syntax/vla_multidim.c
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 4e88edb64f0..c77af9cb63b 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -5171,7 +5171,9 @@ and doType (ghost:bool) isFuncArg
Cil_printer.pp_exp cst
else
Kernel.error ~once:true ~current:true
- "Array length %a is not a compile-time constant."
+ "Array length %a is not a compile-time constant,@ \
+ and currently VLAs may only have their first dimension \
+ as variable."
Cil_printer.pp_exp cst
| _ -> ());
if Cil.isZero len' && not allowZeroSizeArrays &&
diff --git a/tests/syntax/oracle/vla_multidim.0.res.oracle b/tests/syntax/oracle/vla_multidim.0.res.oracle
new file mode 100644
index 00000000000..e8c8d97b725
--- /dev/null
+++ b/tests/syntax/oracle/vla_multidim.0.res.oracle
@@ -0,0 +1,32 @@
+[kernel] Parsing tests/syntax/vla_multidim.c (with preprocessing)
+/* Generated by Frama-C */
+int const n = 10;
+/*@ assigns \nothing;
+ frees p; */
+ __attribute__((__FC_BUILTIN__)) void __fc_vla_free(void *p);
+
+/*@ assigns \result;
+ assigns \result \from \nothing;
+ allocates \result; */
+ __attribute__((__FC_BUILTIN__)) void *__fc_vla_alloc(unsigned int size);
+
+void main(void)
+{
+ unsigned int __lengthof_a;
+ unsigned int __lengthof_b;
+ /*@ assert alloca_bounds: 0 < sizeof(int [42]) * n ≤ 4294967295; */ ;
+ __lengthof_a = (unsigned int)n;
+ int (*a)[42] = __fc_vla_alloc(sizeof(int [42]) * __lengthof_a);
+ (*(a + 0))[0] = 1;
+ /*@
+ assert
+ alloca_bounds: 0 < sizeof(int [5][10]) * (*(a + 0))[0] ≤ 4294967295; */
+ ;
+ __lengthof_b = (unsigned int)(*(a + 0))[0];
+ int (*b)[5][10] = __fc_vla_alloc(sizeof(int [5][10]) * __lengthof_b);
+ __fc_vla_free((void *)b);
+ __fc_vla_free((void *)a);
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/vla_multidim.1.res.oracle b/tests/syntax/oracle/vla_multidim.1.res.oracle
new file mode 100644
index 00000000000..8e04a9a35c6
--- /dev/null
+++ b/tests/syntax/oracle/vla_multidim.1.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing tests/syntax/vla_multidim.c (with preprocessing)
+[kernel] tests/syntax/vla_multidim.c:15: User Error:
+ Array length n is not a compile-time constant,
+ and currently VLAs may only have their first dimension as variable.
+[kernel] tests/syntax/vla_multidim.c:16: User Error:
+ Array length n is not a compile-time constant,
+ and currently VLAs may only have their first dimension as variable.
+[kernel] tests/syntax/vla_multidim.c:17: User Error:
+ Array length n is not a compile-time constant,
+ and currently VLAs may only have their first dimension as variable.
+[kernel] User Error: stopping on file "tests/syntax/vla_multidim.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/vla_multidim.c b/tests/syntax/vla_multidim.c
new file mode 100644
index 00000000000..8308e048384
--- /dev/null
+++ b/tests/syntax/vla_multidim.c
@@ -0,0 +1,19 @@
+/* run.config
+ STDOPT: #""
+ EXIT: 1
+ STDOPT: #"-cpp-extra-args=-DMULTIVLA"
+*/
+
+const int n = 10;
+
+void main() {
+ int a[n][42]; // single variable length dimension
+ a[0][0] = 1;
+ int b[a[0][0]][5][10]; // idem
+#ifdef MULTIVLA
+ // arrays with non-first variable dimensions; not currently supported
+ int c[n][n];
+ int d[42][n];
+ int e[1][n][9];
+#endif
+}
--
GitLab