diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 471bf33f62c10109b6778b760901dc5eb19a9dc3..826000ae54ffa9595eedb80f6b79a4ffc35b6861 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -3040,11 +3040,9 @@ let rec collectInitializer
| Some len -> begin
match constFoldToInt len with
| Some ni when Integer.ge ni Integer.zero -> to_integer ni, false
- | _ ->
- abort_context
- "Array length %a is not a compile-time constant: \
- no explicit initializer allowed."
- Cil_printer.pp_exp len
+ | _ -> (* VLA cannot have initializers, and this should have
+ been captured beforehand. *)
+ Kernel.fatal "Trying to initialize a variable-length array"
end
| _ ->
(* unsized array case, length comes from initializers *)
@@ -3980,6 +3978,11 @@ let get_lval_compound_assigned op expr =
Cil_printer.pp_lval x
| _ -> abort_context "Expected lval for %s" op
+type var_decl_kind =
+ [ `FormalDecl | `GlobalDecl | `LocalDecl | `LocalStaticDecl ]
+type type_context =
+ [ var_decl_kind | `FieldDecl | `Typedef | `OnlyType ]
+
(* The way formals are handled now might generate incorrect types, in the
sense that they refer to a varinfo (in the case of VLA depending on a
previously declared formal) that exists only during the call to doType.
@@ -4448,8 +4451,7 @@ let rec doSpecList loc ghost (suggestedAnonName: string)
*)
t'
- | [Cabs.TtypeofT (specs, dt)] ->
- doOnlyType loc ghost specs dt
+ | [Cabs.TtypeofT (specs, dt)] -> doOnlyType loc ghost specs dt
| l ->
abort_context
@@ -4471,21 +4473,22 @@ and convertCVtoAttr (src: Cabs.cvspec list) : Cabs.attribute list =
and makeVarInfoCabs
~(ghost:bool)
- ~(isformal: bool)
- ~(isglobal: bool)
+ ~(kind:var_decl_kind)
?(isgenerated=false)
?(referenced=false)
(ldecl : location)
(bt, sto, inline, attrs)
(n,ndt,a)
: varinfo =
+ let isglobal = kind = `GlobalDecl || kind = `LocalStaticDecl in
+ let isformal = kind = `FormalDecl in
let vtype, nattr =
- doType ghost isformal (AttrName false)
- ~allowVarSizeArrays:isformal (* For locals we handle var-sized arrays
- before makeVarInfoCabs; for formals
- we do it afterwards *)
- bt (Cabs.PARENTYPE(attrs, ndt, a)) in
- (*Format.printf "Got yp:%a->%a(%a)@." d_type bt d_type vtype d_attrlist nattr;*)
+ doType ghost (kind:>type_context) (AttrName false)
+ ~allowVarSizeArrays:isformal
+ (* For locals we handle var-sized arrays before makeVarInfoCabs;
+ Hence, at this point only formals can have a VLA type *)
+ bt (Cabs.PARENTYPE(attrs, ndt, a))
+ in
if hasAttribute "thread" nattr then begin
let wkey = Kernel.wkey_inconsistent_specifier in
let source = fst ldecl in
@@ -4509,17 +4512,13 @@ and makeVarInfoCabs
if inline && not (isFunctionType vtype) then
Kernel.error ~once:true ~current:true "inline for a non-function: %s" n;
checkRestrictQualifierDeep vtype;
- (* log "Looking at %s(%b): (%a)@." n isformal d_attrlist nattr;*)
- let vi = makeVarinfo ~ghost ~referenced ~temp:isgenerated ~loc:ldecl isglobal isformal n vtype
+ let vi =
+ makeVarinfo ~ghost ~referenced ~temp:isgenerated ~loc:ldecl isglobal isformal n vtype
in
vi.vstorage <- sto;
vi.vattr <- nattr;
vi.vdefined <-
not (isFunctionType vtype) && isglobal && (sto = NoStorage || sto = Static);
-
- (* if false then
- log "Created varinfo %s : %a\n" vi.vname d_type vi.vtype;*)
-
vi
(* Process a local variable declaration and allow variable-sized arrays *)
@@ -4527,12 +4526,12 @@ and makeVarSizeVarInfo ghost (ldecl : location)
spec_res
(n,ndt,a)
: varinfo * chunk * exp * bool =
+ let kind = `LocalDecl in
if not (Cil.msvcMode ()) then
match isVariableSizedArray ghost ndt with
| None ->
- makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:false
- ldecl spec_res (n,ndt,a), empty, zero ~loc:ldecl, false
+ makeVarInfoCabs ~ghost ~kind ldecl spec_res (n,ndt,a),
+ empty, zero ~loc:ldecl, false
| Some (ndt', se, len) ->
(* In this case, we have changed the type from VLA to pointer: add the
qualifier to the elements. *)
@@ -4541,13 +4540,10 @@ and makeVarSizeVarInfo ghost (ldecl : location)
(t, sto , inline , ("ghost", []) :: attrs)
| normal -> normal
in
- makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:false
- ldecl spec_res (n,ndt',a), se, len, true
+ makeVarInfoCabs ~ghost ~kind ldecl spec_res (n,ndt',a), se, len, true
else
- makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:false
- ldecl spec_res (n,ndt,a), empty, zero ~loc:ldecl, false
+ makeVarInfoCabs ~ghost ~kind ldecl spec_res (n,ndt,a),
+ empty, zero ~loc:ldecl, false
and doAttr ghost (a: Cabs.attribute) : attribute list =
(* Strip the leading and trailing underscore *)
@@ -4671,9 +4667,7 @@ and cabsPartitionAttributes
in
loop ([], [], []) attrs
-
-
-and doType (ghost:bool) isFuncArg
+and doType (ghost:bool) (context: type_context)
(nameortype: attributeClass) (* This is AttrName if we are doing
* the type for a name, or AttrType
* if we are doing this type in a
@@ -4698,10 +4692,7 @@ and doType (ghost:bool) isFuncArg
let a1n, a1f, a1t = partitionAttributes ~default:AttrType a1' in
let a2' = doAttributes ghost a2 in
let a2n, a2f, a2t = partitionAttributes ~default:nameortype a2' in
- (*Format.printf "doType: @[a1n=%a@\na1f=%a@\na1t=%a@\na2n=%a@\na2f=%a@\na2t=%a@]@\n" d_attrlist a1n d_attrlist a1f d_attrlist a1t d_attrlist a2n d_attrlist a2f d_attrlist a2t;*)
let bt' = cabsTypeAddAttributes a1t bt in
- (* log "bt' = %a@." d_type bt';*)
-
let bt'', a1fadded =
match unrollType bt with
| TFun _ -> cabsTypeAddAttributes a1f bt', true
@@ -4737,7 +4728,6 @@ and doType (ghost:bool) isFuncArg
Cil_printer.pp_attributes a2f;
restyp
in
- (* log "restyp' = %a@." d_type restyp';*)
(* Now add the name attributes and return *)
restyp', cabsAddAttributes a1n (cabsAddAttributes a2n nattr)
@@ -4848,12 +4838,28 @@ and doType (ghost:bool) isFuncArg
"Unable to do constant-folding on array length %a. \
Some CIL operations on this array may fail."
Cil_printer.pp_exp cst
- else
- Kernel.error ~once:true ~current:true
- "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
+ else begin
+ match context with
+ | `FieldDecl ->
+ Kernel.error ~once:true ~current:true
+ "\"Variable length array in structure\" extension \
+ is not supported"
+ | `GlobalDecl ->
+ Kernel.error ~once:true ~current:true
+ "Global arrays cannot have variable size"
+ | `LocalStaticDecl ->
+ Kernel.error ~once:true ~current:true
+ "Static arrays cannot have variable size"
+ | `Typedef ->
+ Kernel.error ~once:true ~current:true
+ "A type definition cannot be a variable-length array"
+ | `LocalDecl ->
+ Kernel.not_yet_implemented
+ "For multi-dimensional arrays, variable length is only \
+ supported on the first dimension"
+ | `OnlyType | `FormalDecl ->
+ Kernel.fatal "VLA should be accepted in this context"
+ end
| _ -> ());
if Cil.isZero len' && not allowZeroSizeArrays &&
not (Cil.gccMode () || Cil.msvcMode ())
@@ -4863,7 +4869,7 @@ and doType (ghost:bool) isFuncArg
Some len'
in
let al' = doAttributes ghost al in
- if not isFuncArg && hasAttribute "static" al' then
+ if context <> `FormalDecl && hasAttribute "static" al' then
Kernel.error ~once:true ~current:true
"static specifier inside array argument is allowed only in \
function argument";
@@ -4900,8 +4906,9 @@ and doType (ghost:bool) isFuncArg
let doOneArg argl_length is_ghost (s, (n, ndt, a, cloc)) : varinfo =
let ghost = is_ghost || ghost in
let s' = doSpecList cloc ghost n s in
- let vi = makeVarInfoCabs ~ghost ~isformal:true ~isglobal:false
- (convLoc cloc) s' (n,ndt,a) in
+ let vi =
+ makeVarInfoCabs ~ghost ~kind:`FormalDecl (convLoc cloc) s' (n,ndt,a)
+ in
if isVoidType vi.vtype then begin
if argl_length > 1 then
Kernel.error ~once:true ~current:true
@@ -5057,12 +5064,14 @@ and isVariableSizedArray ghost (dt: Cabs.decl_type)
| None -> None
| Some (se, e) -> Some (dt', se, e)
-and doOnlyType loc ghost (specs: Cabs.spec_elem list) (dt: Cabs.decl_type) : typ =
+and doOnlyType loc ghost specs dt =
let bt',sto,inl,attrs = doSpecList loc ghost "" specs in
if sto <> NoStorage || inl then
Kernel.error ~once:true ~current:true "Storage or inline specifier in type only";
let tres, nattr =
- doType ghost false AttrType bt' (Cabs.PARENTYPE(attrs, dt, [])) in
+ doType ghost `OnlyType AttrType bt' (Cabs.PARENTYPE(attrs, dt, []))
+ ~allowVarSizeArrays:true
+ in
if nattr <> [] then
Kernel.error ~once:true ~current:true
"Name attributes in only_type: %a" Cil_printer.pp_attributes nattr;
@@ -5106,7 +5115,7 @@ and makeCompType loc ghost (isstruct: bool)
let allowZeroSizeArrays = Cil.gccMode () || Cil.msvcMode () in
let ftype, fattr =
doType
- ~allowZeroSizeArrays ghost false (AttrName false) bt
+ ~allowZeroSizeArrays ghost `FieldDecl (AttrName false) bt
(Cabs.PARENTYPE(attrs, ndt, a))
in
(* check for fields whose type is incomplete. In particular, this rules
@@ -8497,8 +8506,10 @@ and createGlobal loc ghost logic_spec ((t,s,b,attr_list) : (typ * storage * bool
in
(* Make a first version of the varinfo *)
let vi_loc = convLoc cloc in
- let vi = makeVarInfoCabs ~ghost ~isformal:false ~referenced:islibc
- ~isglobal:true ~isgenerated vi_loc (t,s,b,attr_list) (n,ndt,a)
+ let vi =
+ makeVarInfoCabs
+ ~ghost ~kind:`GlobalDecl ~referenced:islibc ~isgenerated
+ vi_loc (t,s,b,attr_list) (n,ndt,a)
in
(* Add the variable to the environment before doing the initializer
* because it might refer to the variable itself *)
@@ -8784,9 +8795,8 @@ and createLocal ghost ((_, sto, _, _) as specs)
in
let newname, _ = newAlphaName ghost true "" full_name in
(* Make it global *)
- let vi = makeVarInfoCabs ~ghost ~isformal:false
- ~isglobal:true
- loc specs (n, ndt, a) in
+ let vi = makeVarInfoCabs ~ghost ~kind:`LocalStaticDecl loc specs (n, ndt, a)
+ in
checkArray inite vi;
vi.vname <- newname;
let attrs = Cil.addAttribute (Attr (fc_local_static,[])) vi.vattr in
@@ -8867,8 +8877,7 @@ and createLocal ghost ((_, sto, _, _) as specs)
let savelen =
makeVarInfoCabs
~ghost
- ~isformal:false
- ~isglobal:false
+ ~kind:`LocalDecl
loc
(theMachine.typeOfSizeOf, NoStorage, false, [])
("__lengthof_" ^ vi.vname,JUSTBASE, [])
@@ -9078,7 +9087,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
if isglobal then begin
let bt,_,_,attrs = spec_res in
let vtype, nattr =
- doType local_env.is_ghost false
+ doType local_env.is_ghost `GlobalDecl
(AttrName false) bt (Cabs.PARENTYPE(attrs, ndt, a)) in
(match filterAttributes "alias" nattr with
| [] -> (* ordinary prototype. *)
@@ -9216,8 +9225,9 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
let bt,sto,inl,attrs = doSpecList idloc local_env.is_ghost n specs in
!currentFunctionFDEC.svar.vinline <- inl;
let ftyp, funattr =
- doType local_env.is_ghost false
- (AttrName false) bt (Cabs.PARENTYPE(attrs, dt, a)) in
+ doType local_env.is_ghost `GlobalDecl
+ (AttrName false) bt (Cabs.PARENTYPE(attrs, dt, a))
+ in
if hasAttribute "thread" funattr then begin
let wkey = Kernel.wkey_inconsistent_specifier in
let source = fst funloc in
@@ -9621,7 +9631,7 @@ and doTypedef ghost ((specs, nl): Cabs.name_group) =
let createTypedef ((n,ndt,a,_) : Cabs.name) =
(* E.s (error "doTypeDef") *)
let newTyp, tattr =
- doType ghost false AttrType bt (Cabs.PARENTYPE(attrs, ndt, a)) in
+ doType ghost `Typedef AttrType bt (Cabs.PARENTYPE(attrs, ndt, a)) in
checkTypedefSize n newTyp;
let tattr = fc_stdlib_attribute tattr in
let newTyp' = cabsTypeAddAttributes tattr newTyp in
@@ -9720,7 +9730,7 @@ and doOnlyTypedef ghost (specs: Cabs.spec_elem list) : unit =
Kernel.error ~once:true ~current:true
"Storage or inline specifier not allowed in typedef";
let restyp, nattr =
- doType ghost false AttrType bt (Cabs.PARENTYPE(attrs, Cabs.JUSTBASE, []))
+ doType ghost `Typedef AttrType bt (Cabs.PARENTYPE(attrs, Cabs.JUSTBASE, []))
in
if nattr <> [] then
Kernel.warning ~current:true "Ignoring identifier attribute";
@@ -10237,7 +10247,7 @@ and doStatement local_env (s : Cabs.statement) : chunk =
let spec = doSpecList ldecl ghost n t in
let vi =
makeVarInfoCabs
- ~ghost ~isformal:false ~isglobal:false ldecl spec (n,ndt,a)
+ ~ghost ~kind:`LocalDecl ldecl spec (n,ndt,a)
in
addLocalToEnv ghost n (EnvVar vi);
!currentFunctionFDEC.slocals <- vi :: !currentFunctionFDEC.slocals;
diff --git a/tests/syntax/array_size.c b/tests/syntax/array_size.c
new file mode 100644
index 0000000000000000000000000000000000000000..89bec6ef204ad5945c9caf79d316c5b8cef37eb0
--- /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 [size][2] = { { 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/generic.c b/tests/syntax/generic.c
index 17726aab534ca3727bd74b063ccb58fd833d160c..15a9d6aa05fa9e4048c736354908ca4f41fe01bc 100644
--- a/tests/syntax/generic.c
+++ b/tests/syntax/generic.c
@@ -9,6 +9,7 @@
STDOPT: #"-cpp-extra-args=-DINCOMPLETE_TYPE"
STDOPT: #"-cpp-extra-args=-DINCOMPATIBLE_QUALIFIED_TYPE"
STDOPT: #"-cpp-extra-args=-DFUNCTION_TYPE"
+ STDOPT: #"-cpp-extra-args=-DVLA"
EXIT: 0
STDOPT:
*/
@@ -63,6 +64,11 @@ int main() {
#endif
#ifdef INCOMPATIBLE_QUALIFIED_TYPE
int a = _Generic("abc", char const *: 0);
+#endif
+#ifdef VLA
+ int x = 42;
+ int y[x];
+ int a = _Generic(y, int[x]: 0, default: 1);
#endif
int ok1 = _Generic("abc", char*: 0);
int ok2 = _Generic(1.0, float: 1, double: 0);
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..fbc09a34ed2aa0b72b59478a488aefe0399326f1
--- /dev/null
+++ b/tests/syntax/oracle/array_size.2.res.oracle
@@ -0,0 +1,6 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:23: 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.3.res.oracle b/tests/syntax/oracle/array_size.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..421d4380a6e78931a60d1830933bb337ae95e7b2
--- /dev/null
+++ b/tests/syntax/oracle/array_size.3.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:30: User Error: Global arrays cannot have variable size
+[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..f18504df1ed797cc2f0f886c37a9da1edc893068
--- /dev/null
+++ b/tests/syntax/oracle/array_size.4.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing array_size.c (with preprocessing)
+[kernel] array_size.c:34: User Error: Global arrays cannot have variable size
+[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.
diff --git a/tests/syntax/oracle/generic.1.res.oracle b/tests/syntax/oracle/generic.1.res.oracle
index c8f6605be6dcb690f616c3dd9bcdf7fc7226ea19..525bed32e1ea201e2fd17042f1b7055ef57eaa50 100644
--- a/tests/syntax/oracle/generic.1.res.oracle
+++ b/tests/syntax/oracle/generic.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:36:
+[kernel] generic.c:37:
_Generic requires at least one generic association:
- Location: line 36, between columns 10 and 25, before or at token: ;
- 34 int main() {
- 35 #ifdef NONE
- 36 int a = _Generic("abc");
+ Location: line 37, between columns 10 and 25, before or at token: ;
+ 35 int main() {
+ 36 #ifdef NONE
+ 37 int a = _Generic("abc");
^^^^^^^^^^^^^^^
- 37 #endif
- 38 #ifdef TOO_MANY_DEFAULTS
+ 38 #endif
+ 39 #ifdef TOO_MANY_DEFAULTS
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.10.res.oracle b/tests/syntax/oracle/generic.10.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..70bdefa20fded77f7906a06abef980f36e8fc77e
--- /dev/null
+++ b/tests/syntax/oracle/generic.10.res.oracle
@@ -0,0 +1,32 @@
+[kernel] Parsing generic.c (with preprocessing)
+/* Generated by Frama-C */
+int foo(int i)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+void void_foo(int i)
+{
+ return;
+}
+
+float cbrtf(float x);
+
+int main(void)
+{
+ int __retres;
+ float tmp;
+ int ok1 = 0;
+ int ok2 = 0;
+ int ok3 = 0;
+ int ok4 = 0;
+ tmp = cbrtf(0.0f);
+ double c = (double)tmp;
+ int ok5 = 0;
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/tests/syntax/oracle/generic.2.res.oracle b/tests/syntax/oracle/generic.2.res.oracle
index 0edc5626dfd5157572f29d022cfbf997a14fba98..592f81d34ca92c28b5b06208ad9812a2b163f9de 100644
--- a/tests/syntax/oracle/generic.2.res.oracle
+++ b/tests/syntax/oracle/generic.2.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:39: User Error:
+[kernel] generic.c:40: User Error:
multiple default clauses in _Generic selection
- 37 #endif
- 38 #ifdef TOO_MANY_DEFAULTS
- 39 int a = _Generic("abc", default: 1, default: 1);
+ 38 #endif
+ 39 #ifdef TOO_MANY_DEFAULTS
+ 40 int a = _Generic("abc", default: 1, default: 1);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 40 #endif
- 41 #ifdef TOO_MANY_COMPATIBLE
+ 41 #endif
+ 42 #ifdef TOO_MANY_COMPATIBLE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.3.res.oracle b/tests/syntax/oracle/generic.3.res.oracle
index af00e69e6f9a9db9d0453d3965d5af3f92f4deb1..89f860800fa257cb2642325739dc2d86ca8c1624 100644
--- a/tests/syntax/oracle/generic.3.res.oracle
+++ b/tests/syntax/oracle/generic.3.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:43: User Error:
+[kernel] generic.c:44: User Error:
multiple compatible types in _Generic selection:
'my_uint' and 'unsigned int'
- 41 #ifdef TOO_MANY_COMPATIBLE
- 42 // compatibility via typedef
- 43 int a = _Generic(42, my_uint: 1, unsigned int: 2);
+ 42 #ifdef TOO_MANY_COMPATIBLE
+ 43 // compatibility via typedef
+ 44 int a = _Generic(42, my_uint: 1, unsigned int: 2);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 44 #endif
- 45 #ifdef TOO_MANY_COMPATIBLE2
+ 45 #endif
+ 46 #ifdef TOO_MANY_COMPATIBLE2
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.4.res.oracle b/tests/syntax/oracle/generic.4.res.oracle
index 4dea267e9f5cf04b162f789e3847a6714d99c8a0..3b8bc64668e46d3130dbeadd94f7436883f59ddb 100644
--- a/tests/syntax/oracle/generic.4.res.oracle
+++ b/tests/syntax/oracle/generic.4.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:47: User Error:
+[kernel] generic.c:48: User Error:
multiple compatible types in _Generic selection:
'void (*)()' and 'void (*)(void)'
- 45 #ifdef TOO_MANY_COMPATIBLE2
- 46 // compatibility modulo implicit arguments
+ 46 #ifdef TOO_MANY_COMPATIBLE2
+ 47 // compatibility modulo implicit arguments
- 47 int a = _Generic(0,
- 48 void (*)(): 0,
- 49 void (*)(void): 0);
+ 48 int a = _Generic(0,
+ 49 void (*)(): 0,
+ 50 void (*)(void): 0);
- 50 #endif
- 51 #ifdef TOO_MANY_COMPATIBLE3
+ 51 #endif
+ 52 #ifdef TOO_MANY_COMPATIBLE3
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.5.res.oracle b/tests/syntax/oracle/generic.5.res.oracle
index 579b9dde7959145550bcea41382a8e721f40b21d..5c1e7279049cc649936e472d3b2b116f1eb5d75f 100644
--- a/tests/syntax/oracle/generic.5.res.oracle
+++ b/tests/syntax/oracle/generic.5.res.oracle
@@ -1,15 +1,15 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:54: User Error:
+[kernel] generic.c:55: User Error:
controlling expression compatible with more than one association type in _Generic selection:
controlling expression: '(void (*)())0' (type: void (*)());
compatible types: void (*)(void), void (*)(int )
- 52 // implicit arguments compatible between first and second selector,
- 53 // but the selectors themselves are not compatible between them
+ 53 // implicit arguments compatible between first and second selector,
+ 54 // but the selectors themselves are not compatible between them
- 54 int a = _Generic((void (*)()) 0,
- 55 void (*)(int): 0,
- 56 void (*)(void): 0);
+ 55 int a = _Generic((void (*)()) 0,
+ 56 void (*)(int): 0,
+ 57 void (*)(void): 0);
- 57 #endif
- 58 #ifdef INCOMPLETE_TYPE
+ 58 #endif
+ 59 #ifdef INCOMPLETE_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.6.res.oracle b/tests/syntax/oracle/generic.6.res.oracle
index fbfffc1be280933ec883e33e343a303d4541dd09..c53dd9c2738d9895b66b26f0f716fc193b587cc6 100644
--- a/tests/syntax/oracle/generic.6.res.oracle
+++ b/tests/syntax/oracle/generic.6.res.oracle
@@ -1,10 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:59: User Error:
+[kernel] generic.c:60: User Error:
generic association with incomplete type 'void'
- 57 #endif
- 58 #ifdef INCOMPLETE_TYPE
- 59 int a = _Generic(42, void: 1, default: 2);
+ 58 #endif
+ 59 #ifdef INCOMPLETE_TYPE
+ 60 int a = _Generic(42, void: 1, default: 2);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 60 #endif
- 61 #ifdef FUNCTION_TYPE
+ 61 #endif
+ 62 #ifdef FUNCTION_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.7.res.oracle b/tests/syntax/oracle/generic.7.res.oracle
index c232c3c417e6f8d49a53f25f9f116dc939d908b2..03f063c8583744504a73b16416ccd9bf9269d900 100644
--- a/tests/syntax/oracle/generic.7.res.oracle
+++ b/tests/syntax/oracle/generic.7.res.oracle
@@ -1,12 +1,12 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:65: User Error:
+[kernel] generic.c:66: User Error:
no compatible types and no default type in _Generic selection:
controlling expression: '"abc"' (type: char *);
candidate types: char const *
- 63 #endif
- 64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
- 65 int a = _Generic("abc", char const *: 0);
+ 64 #endif
+ 65 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
+ 66 int a = _Generic("abc", char const *: 0);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
- 66 #endif
- 67 int ok1 = _Generic("abc", char*: 0);
+ 67 #endif
+ 68 #ifdef VLA
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.8.res.oracle b/tests/syntax/oracle/generic.8.res.oracle
index fe35717281298c85c4a8ef02888473d4a3b90dce..78569285df29b0e24c4d302c3e8ec06023d6ca9c 100644
--- a/tests/syntax/oracle/generic.8.res.oracle
+++ b/tests/syntax/oracle/generic.8.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing generic.c (with preprocessing)
-[kernel] generic.c:62:
+[kernel] generic.c:63:
syntax error:
- Location: line 62, column 27, before or at token: int
- 60 #endif
- 61 #ifdef FUNCTION_TYPE
- 62 int a = _Generic(1, void(int): 1);
+ Location: line 63, column 27, before or at token: int
+ 61 #endif
+ 62 #ifdef FUNCTION_TYPE
+ 63 int a = _Generic(1, void(int): 1);
^
- 63 #endif
- 64 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
+ 64 #endif
+ 65 #ifdef INCOMPATIBLE_QUALIFIED_TYPE
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/generic.9.res.oracle b/tests/syntax/oracle/generic.9.res.oracle
index 70bdefa20fded77f7906a06abef980f36e8fc77e..ef373d91c17e019395537108fc0b5d486723d6a9 100644
--- a/tests/syntax/oracle/generic.9.res.oracle
+++ b/tests/syntax/oracle/generic.9.res.oracle
@@ -1,32 +1,10 @@
[kernel] Parsing generic.c (with preprocessing)
-/* Generated by Frama-C */
-int foo(int i)
-{
- int __retres;
- __retres = 0;
- return __retres;
-}
-
-void void_foo(int i)
-{
- return;
-}
-
-float cbrtf(float x);
-
-int main(void)
-{
- int __retres;
- float tmp;
- int ok1 = 0;
- int ok2 = 0;
- int ok3 = 0;
- int ok4 = 0;
- tmp = cbrtf(0.0f);
- double c = (double)tmp;
- int ok5 = 0;
- __retres = 0;
- return __retres;
-}
-
-
+[kernel] generic.c:71: User Error:
+ generic association with variably modified type 'int [x]'
+ 69 int x = 42;
+ 70 int y[x];
+ 71 int a = _Generic(y, int[x]: 0, default: 1);
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 72 #endif
+ 73 int ok1 = _Generic("abc", char*: 0);
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/sizeof.0.res.oracle b/tests/syntax/oracle/sizeof.0.res.oracle
index aa1ba789ca9fca267ec802decd82a0ed1c226e9d..4eb800ca12dab45e1da5907e8bb2d64eaaca7983 100644
--- a/tests/syntax/oracle/sizeof.0.res.oracle
+++ b/tests/syntax/oracle/sizeof.0.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing sizeof.c (with preprocessing)
/* Generated by Frama-C */
+#include "assert.h"
#include "stdint.h"
char c = (char)1;
char a = (char)'a';
@@ -14,4 +15,12 @@ uint64_t u64 = 6453UL;
int v = 645201;
float f = (float)1.;
double d = 1.;
+void vla(int n)
+{
+ unsigned long s = sizeof(int [n]);
+ __FC_assert((s == (unsigned long)n * sizeof(int)) != 0,"sizeof.c",49,
+ "s == n * sizeof(int)");
+ return;
+}
+
diff --git a/tests/syntax/oracle/sizeof.1.res.oracle b/tests/syntax/oracle/sizeof.1.res.oracle
index 05c8abe3fa6d930520097aa9c3b94a8f07000f3e..f66dc175d39c9a6d08950bd025d00bf455a6c564 100644
--- a/tests/syntax/oracle/sizeof.1.res.oracle
+++ b/tests/syntax/oracle/sizeof.1.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing sizeof.c (with preprocessing)
/* Generated by Frama-C */
+#include "assert.h"
#include "stdint.h"
char c = (char)1;
char a = (char)'a';
@@ -14,4 +15,12 @@ uint64_t u64 = 6453ULL;
int v = 645201;
float f = (float)1.;
double d = 1.;
+void vla(int n)
+{
+ unsigned long s = (unsigned long)sizeof(int [n]);
+ __FC_assert((s == (unsigned long)((unsigned int)n * sizeof(int))) != 0,
+ "sizeof.c",49,"s == n * sizeof(int)");
+ return;
+}
+
diff --git a/tests/syntax/oracle/vla_multidim.1.res.oracle b/tests/syntax/oracle/vla_multidim.1.res.oracle
index 09f9c527f3c5e955e651df57f5b5967bba4f1a8a..aa97a0bb5c6ca726925a4e3bc7ac37cb9fc1c8af 100644
--- a/tests/syntax/oracle/vla_multidim.1.res.oracle
+++ b/tests/syntax/oracle/vla_multidim.1.res.oracle
@@ -1,13 +1,4 @@
[kernel] Parsing vla_multidim.c (with preprocessing)
-[kernel] 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] 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] 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 "vla_multidim.c" that has errors. Add '-kernel-msg-key pp'
- for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Frama-C aborted: unimplemented feature.
+ You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
+ '[Frama-C] For multi-dimensional arrays, variable length is only supported on the first dimension'.
diff --git a/tests/syntax/oracle/vla_multidim.2.res.oracle b/tests/syntax/oracle/vla_multidim.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..aa97a0bb5c6ca726925a4e3bc7ac37cb9fc1c8af
--- /dev/null
+++ b/tests/syntax/oracle/vla_multidim.2.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing vla_multidim.c (with preprocessing)
+[kernel] Frama-C aborted: unimplemented feature.
+ You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
+ '[Frama-C] For multi-dimensional arrays, variable length is only supported on the first dimension'.
diff --git a/tests/syntax/oracle/vla_multidim.3.res.oracle b/tests/syntax/oracle/vla_multidim.3.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..aa97a0bb5c6ca726925a4e3bc7ac37cb9fc1c8af
--- /dev/null
+++ b/tests/syntax/oracle/vla_multidim.3.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing vla_multidim.c (with preprocessing)
+[kernel] Frama-C aborted: unimplemented feature.
+ You may send a feature request at https://git.frama-c.com/pub/frama-c/issues with:
+ '[Frama-C] For multi-dimensional arrays, variable length is only supported on the first dimension'.
diff --git a/tests/syntax/sizeof.c b/tests/syntax/sizeof.c
index a27bf94011e4a4341faf3a7e948d360ce70ec2d4..7fbc16abc9fc42a0b75856d8b054f318582f9da1 100644
--- a/tests/syntax/sizeof.c
+++ b/tests/syntax/sizeof.c
@@ -3,6 +3,9 @@
STDOPT: -machdep x86_64
STDOPT: -machdep x86_32
*/
+
+#include <assert.h>
+
char c = 1;
_Static_assert(sizeof(-c) == sizeof(int), "Integer promotion with minus");
_Static_assert(sizeof(+c) == sizeof(int), "Integer promotion with plus");
@@ -40,3 +43,8 @@ float f = 1.;
_Static_assert(sizeof +f == sizeof(float), "Float promotion");
double d = 1.;
_Static_assert(sizeof +d == sizeof(double), "Double promotion");
+
+void vla(int n) {
+ unsigned long s = sizeof(int[n]);
+ assert(s == n * sizeof(int));
+}
diff --git a/tests/syntax/vla_multidim.c b/tests/syntax/vla_multidim.c
index 8308e0483842a31af16107b276f1398642f3acdf..e2c6c75e21bf1e03b0a0188067399a74cb67bbec 100644
--- a/tests/syntax/vla_multidim.c
+++ b/tests/syntax/vla_multidim.c
@@ -1,7 +1,9 @@
/* run.config
STDOPT: #""
- EXIT: 1
- STDOPT: #"-cpp-extra-args=-DMULTIVLA"
+ EXIT: 3
+ STDOPT: #"-cpp-extra-args=-DMULTIVLA1"
+ STDOPT: #"-cpp-extra-args=-DMULTIVLA2"
+ STDOPT: #"-cpp-extra-args=-DMULTIVLA3"
*/
const int n = 10;
@@ -10,10 +12,15 @@ 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
+
+// arrays with non-first variable dimensions; not currently supported
+#ifdef MULTIVLA1
int c[n][n];
- int d[42][n];
+#endif
+#ifdef MULTIVLA2
+int d[42][n];
+#endif
+#ifdef MULTIVLA3
int e[1][n][9];
#endif
}