diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 4e88edb64f0ffd77e8db0f1dc49f208b0e94263c..c77af9cb63bd8e5d454b7e2e5e588af8f820ec46 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 0000000000000000000000000000000000000000..e8c8d97b725aa8500b49c427eb3c866c6859c845 --- /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 0000000000000000000000000000000000000000..8e04a9a35c64380a69e8f6c69a3e2962c00ab593 --- /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 0000000000000000000000000000000000000000..8308e0483842a31af16107b276f1398642f3acdf --- /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 +}