diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 52363c334d273e63d71545af7b2251e83f5a04b1..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 %s" op (Cil.onlyOnGccMsvc false);
+ 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 %s" op (Cil.onlyOnGccMsvc true);
+ 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 %s" (Cil.onlyOnGccMsvc true)
+ 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 %s" (Cil.onlyOnGccMsvc true);
+ "zero-length arrays %s" (allowed_machdep "GCC/MSVC");
Some len'
in
let al' = doAttributes ghost al in
@@ -5473,7 +5481,7 @@ and makeCompType ghost (isstruct: bool)
Kernel.error ~source
"field `%s' declared with a type containing a flexible array \
member %s."
- n (Cil.onlyOnGccMsvc true)
+ n (allowed_machdep "GCC/MSVC")
end
else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype)
then begin
@@ -5617,7 +5625,7 @@ and makeCompType ghost (isstruct: bool)
Kernel.error ~current:true ~once:true
"empty %ss %s"
(if comp.cstruct then "struct" else "union")
- (Cil.onlyOnGccMsvc true);
+ (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/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 9f2130864a13d4b14175e39488ba06333e5fa56c..e40b51a88db810af67d5bbcdc17dbfe36bf3861d 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -2955,12 +2955,6 @@ let startsWith prefix s =
let prefixLen = String.length prefix in
String.length s >= prefixLen && String.sub s 0 prefixLen = prefix
-let onlyOnGccMsvc msvc =
- Format.asprintf "only allowed for %s machdeps;@ \
- see option -machdep or@ \
- run '-machdep help' for the list of available machdeps"
- (if msvc then "GCC/MSVC" else "GCC")
-
let bytesSizeOfInt (ik: ikind): int =
match ik with
| IChar | ISChar | IUChar | IBool -> 1
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 0bdc823d851ee5baeb48b01fd8a8df1b1abfd3c5..6b051a1e72eb2d5ec4b1d6a27bb80e0f12756dcc 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -2246,13 +2246,6 @@ val mapNoCopyList: ('a -> 'a list) -> 'a list -> 'a list
(** sm: return true if the first is a prefix of the second string *)
val startsWith: string -> string -> bool
-(** Append the "only allowed on GCC/MSVC machdeps" error message.
- The bool parameter tells whether MSVC should be included in the message
- (otherwise, print just GCC).
- @since Frama-C+dev
-*)
-val onlyOnGccMsvc: bool -> string
-
(* ************************************************************************* *)
(** {2 An Interpreter for constructing CIL constructs} *)
(* ************************************************************************* *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 5a5a11d7d9017232cd78bd9e4e2c53ed8c19b4d8..58725f9e485194a4728aa0724c1a5ed92bd30b7b 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -102,10 +102,9 @@ 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 %s.@ 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
- (Cil.onlyOnGccMsvc true)
| _ -> ()
diff --git a/tests/value/oracle/array_zero_length.2.res.oracle b/tests/value/oracle/array_zero_length.2.res.oracle
index 5e6d5f9a5ed625b20b9c64747cd3fb39eb8e27c8..d040ef54d2c59cb19a5388851d53bc1a322adda6 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -9,7 +9,7 @@
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 only allowed for GCC/MSVC machdeps; see option -machdep or
+ 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
diff --git a/tests/value/oracle/empty_base.1.res.oracle b/tests/value/oracle/empty_base.1.res.oracle
index d1ff8c38bb46c69561bd8d66fc7292d5c87a6731..71459a15f4fc846f3e3efe5f6af2ec0f198efcb5 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -6,7 +6,7 @@
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 only allowed for GCC/MSVC machdeps; see option -machdep or
+ 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];