diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 36f0167b48f18ce13b054dc6b766dca3975af7cb..75665dec0631f0844c434e7dacb8be41d85acee8 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -1349,12 +1349,20 @@ let canDropStatement (s: stmt) : bool =
ignore (visitCilStmt vis s);
!pRes
+let allowed_machdep machdep =
+ Format.asprintf
+ "only allowed for %s machdeps;@ see option -machdep or@ \
+ run '-machdep help' for the list of available machdeps"
+ machdep
+
let fail_if_incompatible_sizeof ~ensure_complete op typ =
if Cil.isFunctionType typ && Cil.theMachine.theMachine.sizeof_fun < 0 then
- Kernel.error ~current:true "%s called on function only allowed for GCC" op;
+ Kernel.error ~current:true "%s called on function %s" op
+ (allowed_machdep "GCC");
let is_void = Cil.isVoidType typ in
if is_void && Cil.theMachine.theMachine.sizeof_void < 0 then
- Kernel.error ~current:true "%s on void type only allowed for GCC/MSVC" op;
+ Kernel.error ~current:true "%s on void type %s" op
+ (allowed_machdep "GCC/MSVC");
if ensure_complete && not (Cil.isCompleteType typ) && not is_void then
Kernel.error ~current:true
"%s on incomplete type '%a'" op Cil_printer.pp_typ typ
@@ -3354,7 +3362,7 @@ let rec _pp_preInit fmt = function
let empty_preinit() =
if Cil.gccMode () || Cil.msvcMode () then
CompoundPre (ref (-1), ref [| |])
- else abort_context "empty initializers only allowed for GCC/MSVC"
+ else abort_context "empty initializers %s" (allowed_machdep "GCC/MSVC")
(* Set an initializer *)
let rec setOneInit this o preinit =
@@ -5207,7 +5215,7 @@ and doType (ghost:bool) isFuncArg
not (Cil.gccMode () || Cil.msvcMode ())
then
Kernel.error ~once:true ~current:true
- "zero-length arrays only allowed for GCC/MSVC";
+ "zero-length arrays %s" (allowed_machdep "GCC/MSVC");
Some len'
in
let al' = doAttributes ghost al in
@@ -5472,8 +5480,8 @@ and makeCompType ghost (isstruct: bool)
else if not (Cil.gccMode() || Cil.msvcMode ()) then
Kernel.error ~source
"field `%s' declared with a type containing a flexible array \
- member only allowed in GCC/MSVC mode."
- n
+ member %s."
+ n (allowed_machdep "GCC/MSVC")
end
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
then begin
@@ -5615,8 +5623,9 @@ and makeCompType ghost (isstruct: bool)
in
if flds = [] && not (Cil.acceptEmptyCompinfo ()) then
Kernel.error ~current:true ~once:true
- "empty %ss only allowed for GCC/MSVC"
- (if comp.cstruct then "struct" else "union");
+ "empty %ss %s"
+ (if comp.cstruct then "struct" else "union")
+ (allowed_machdep "GCC/MSVC");
List.iter check flds;
if comp.cfields <> None then begin
let old_fields = Option.get comp.cfields in
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 4b5bc5babc0439df5f2b280692b404430064d0d0..58725f9e485194a4728aa0724c1a5ed92bd30b7b 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -102,7 +102,7 @@ let reject_empty_struct b offset typ =
if ci.cfields = Some [] && not (Cil.acceptEmptyCompinfo ()) then
Value_parameters.abort ~current:true
"@[empty %ss@ are unsupported@ (type '%a',@ location %a%a)@ \
- in C99 (only allowed as GCC/MSVC extension).@ Aborting.@]"
+ in C99 (only allowed on GCC/MSVC machdep).@ Aborting.@]"
(if ci.cstruct then "struct" else "union")
Printer.pp_typ typ Base.pretty b Printer.pp_offset offset
| _ -> ()
diff --git a/tests/misc/oracle/function_ptr_alignof.res.oracle b/tests/misc/oracle/function_ptr_alignof.res.oracle
index 7e77e91ce97bcc58d4f6a4336b282e51c09b84d1..2348fb1708918c641f35b67bde71af7d34495941 100644
--- a/tests/misc/oracle/function_ptr_alignof.res.oracle
+++ b/tests/misc/oracle/function_ptr_alignof.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing tests/misc/function_ptr_alignof.i (no preprocessing)
[kernel] tests/misc/function_ptr_alignof.i:13: User Error:
- alignof() called on function only allowed for GCC
+ alignof() called on function only allowed for GCC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "tests/misc/function_ptr_alignof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/misc/oracle/function_ptr_sizeof.res.oracle b/tests/misc/oracle/function_ptr_sizeof.res.oracle
index 689d2ad92fa90c5ef6b31140efaaaa65cee65b6b..7a5ccd1565a6b3a9d6852fd41d11d00120e746f3 100644
--- a/tests/misc/oracle/function_ptr_sizeof.res.oracle
+++ b/tests/misc/oracle/function_ptr_sizeof.res.oracle
@@ -1,5 +1,6 @@
[kernel] Parsing tests/misc/function_ptr_sizeof.i (no preprocessing)
[kernel] tests/misc/function_ptr_sizeof.i:13: User Error:
- sizeof() called on function only allowed for GCC
+ sizeof() called on function only allowed for GCC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "tests/misc/function_ptr_sizeof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
index 09f6142e6ee268b2a09e35a7da9a3bbe87c3c745..8fb5b4d7a04dbae50ae63b26ed56f998bb9f5cef 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
@@ -1,6 +1,7 @@
[kernel] Parsing tests/syntax/flexible_array_member_invalid5.i (no preprocessing)
[kernel] tests/syntax/flexible_array_member_invalid5.i:15: User Error:
- field `f' declared with a type containing a flexible array member only allowed in GCC/MSVC mode.
+ field `f' declared with a type containing a flexible array member only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps.
[kernel] User Error: stopping on file "tests/syntax/flexible_array_member_invalid5.i" that has
errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/sizeof_void.0.res.oracle b/tests/syntax/oracle/sizeof_void.0.res.oracle
index f4d8b52e9da0396bbc147a9c32e187c15cc803f4..3b2dc7e8bc4cc02a0f40e2b474f25d26828d2c93 100644
--- a/tests/syntax/oracle/sizeof_void.0.res.oracle
+++ b/tests/syntax/oracle/sizeof_void.0.res.oracle
@@ -1,12 +1,16 @@
[kernel] Parsing tests/syntax/sizeof_void.c (with preprocessing)
[kernel] tests/syntax/sizeof_void.c:9: User Error:
- sizeof on void type only allowed for GCC/MSVC
+ sizeof on void type only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] tests/syntax/sizeof_void.c:16: User Error:
- sizeof() on void type only allowed for GCC/MSVC
+ sizeof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] tests/syntax/sizeof_void.c:21: User Error:
- alignof on void type only allowed for GCC/MSVC
+ alignof on void type only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] tests/syntax/sizeof_void.c:28: User Error:
- alignof() on void type only allowed for GCC/MSVC
+ alignof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "tests/syntax/sizeof_void.c" that has errors. Add
'-kernel-msg-key pp' for preprocessing command.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/array_zero_length.2.res.oracle b/tests/value/oracle/array_zero_length.2.res.oracle
index d5eb6f33988efe8fe86ec90a88f5012364e1e7c6..d040ef54d2c59cb19a5388851d53bc1a322adda6 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -1,13 +1,16 @@
[kernel] Parsing tests/value/array_zero_length.i (no preprocessing)
[kernel] tests/value/array_zero_length.i:9: User Error:
- zero-length arrays only allowed for GCC/MSVC
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] tests/value/array_zero_length.i:11: User Error:
- zero-length arrays only allowed for GCC/MSVC
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] tests/value/array_zero_length.i:11: User Error:
declaration of array of 'zero-length arrays' ('char [0]`);
zero-length arrays are not allowed in C99
[kernel] tests/value/array_zero_length.i:13: User Error:
- empty initializers only allowed for GCC/MSVC
+ empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
11 char W[][0];
12
13 char T1[] = {};
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index d20639084b8ef275e8ff05de7e5179670ad8a54a..71459a15f4fc846f3e3efe5f6af2ec0f198efcb5 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -1,10 +1,13 @@
[kernel] Parsing tests/value/empty_base.c (with preprocessing)
[kernel] tests/value/empty_base.c:13: User Error:
- empty structs only allowed for GCC/MSVC
+ empty structs only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] tests/value/empty_base.c:48: User Error:
- zero-length arrays only allowed for GCC/MSVC
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
[kernel] tests/value/empty_base.c:50: User Error:
- empty initializers only allowed for GCC/MSVC
+ empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or
+ run '-machdep help' for the list of available machdeps
48 struct empty empty_array_of_empty[0];
49 struct empty array_of_empty[1];
50 struct empty many_empty[3] = {{}};