diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index daae7bfac546a9972ea6f529488d8f9a7511a9cb..1b32804d971d3426a76bce64d16f1a4a0e9aa8e2 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -171,8 +171,8 @@ let acceptEmptyCompinfo () =
let allowed_machdep machdep =
Format.asprintf
- "only allowed for %s machdeps;@ see option -machdep or@ \
- run '-machdep help' for the list of available machdeps"
+ "only allowed for %s machdeps; see option -machdep or \
+ run 'frama-c -machdep help' for the list of available machdeps"
machdep
let theMachineProject = ref (createMachine ())
diff --git a/tests/misc/oracle/function_ptr_alignof.res.oracle b/tests/misc/oracle/function_ptr_alignof.res.oracle
index fa223563fb4e588997e95f7fee1b314ec2c92b0e..c25dcf5f2d7b15f305cca1a86fb38435120a3078 100644
--- a/tests/misc/oracle/function_ptr_alignof.res.oracle
+++ b/tests/misc/oracle/function_ptr_alignof.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing function_ptr_alignof.i (no preprocessing)
[kernel] function_ptr_alignof.i:13: User Error:
- alignof() called on function only allowed for GCC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ alignof() called on function only allowed for GCC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "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 06996432c675f999cba76b50b0b13b2e72083267..3f66d533ba61c68d95e83705e0ba3ca5ad41afc3 100644
--- a/tests/misc/oracle/function_ptr_sizeof.res.oracle
+++ b/tests/misc/oracle/function_ptr_sizeof.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing function_ptr_sizeof.i (no preprocessing)
[kernel] function_ptr_sizeof.i:13: User Error:
- sizeof() called on function only allowed for GCC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ sizeof() called on function only allowed for GCC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "function_ptr_sizeof.i" that has errors.
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/compiler_builtins.0.res.oracle b/tests/syntax/oracle/compiler_builtins.0.res.oracle
index 6c6a5186deee9987cd8db54445b900872bd973d3..962db45f53cb5561a0deb60970e2613d548793c1 100644
--- a/tests/syntax/oracle/compiler_builtins.0.res.oracle
+++ b/tests/syntax/oracle/compiler_builtins.0.res.oracle
@@ -1,10 +1,8 @@
[kernel] Parsing compiler_builtins.c (with preprocessing)
[kernel:typing:implicit-function-declaration] compiler_builtins.c:22: Warning:
- __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel:typing:implicit-function-declaration] compiler_builtins.c:25: Warning:
- __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
/* Generated by Frama-C */
#include "stdarg.h"
/* compiler builtin:
diff --git a/tests/syntax/oracle/compiler_builtins.1.res.oracle b/tests/syntax/oracle/compiler_builtins.1.res.oracle
index 0acfe18adc197fe809f31ac5a89e4ee723ad9d7c..d3cf8ba1bb5ad1cc0fe1cdac0ccb120a283ab22d 100644
--- a/tests/syntax/oracle/compiler_builtins.1.res.oracle
+++ b/tests/syntax/oracle/compiler_builtins.1.res.oracle
@@ -1,7 +1,6 @@
[kernel] Parsing compiler_builtins.c (with preprocessing)
[kernel:typing:implicit-function-declaration] compiler_builtins.c:25: Warning:
- __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ __builtin__annotation is a compiler builtin, only allowed for MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
/* Generated by Frama-C */
#include "stdarg.h"
/* compiler builtin:
diff --git a/tests/syntax/oracle/compiler_builtins.2.res.oracle b/tests/syntax/oracle/compiler_builtins.2.res.oracle
index bdd362de6634afe39fca0b06a89f39de32e944e4..cc838d9c9cda183f69fbda4630ecf2522fd5f223 100644
--- a/tests/syntax/oracle/compiler_builtins.2.res.oracle
+++ b/tests/syntax/oracle/compiler_builtins.2.res.oracle
@@ -1,13 +1,10 @@
[kernel] Parsing compiler_builtins.c (with preprocessing)
[kernel:typing:implicit-function-declaration] compiler_builtins.c:16: Warning:
- __builtin_va_start is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ __builtin_va_start is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel:typing:implicit-function-declaration] compiler_builtins.c:17: Warning:
- __builtin_va_end is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ __builtin_va_end is a compiler builtin, only allowed for not MSVC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel:typing:implicit-function-declaration] compiler_builtins.c:22: Warning:
- __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ __builtin_expect is a compiler builtin, only allowed for GCC-based machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
/* Generated by Frama-C */
#include "stdarg.h"
/* compiler builtin:
diff --git a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
index 8f91488188b6cb3016ee725eb2f25ea96c38bd2f..22cf6e91dadcdb16d2f811aa88e9247b8b4730c4 100644
--- a/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
+++ b/tests/syntax/oracle/flexible_array_member_invalid5.res.oracle
@@ -1,6 +1,5 @@
[kernel] Parsing flexible_array_member_invalid5.i (no preprocessing)
[kernel] flexible_array_member_invalid5.i:15: User Error:
- 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.
+ field `f' declared with a type containing a flexible array member only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps.
[kernel] User Error: stopping on file "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 03f35c1ead217d855a3261324725e1624285c621..9ad43d07487edb653606707fc19113361b096509 100644
--- a/tests/syntax/oracle/sizeof_void.0.res.oracle
+++ b/tests/syntax/oracle/sizeof_void.0.res.oracle
@@ -1,16 +1,12 @@
[kernel] Parsing sizeof_void.c (with preprocessing)
[kernel] sizeof_void.c:9: User Error:
- sizeof on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ sizeof on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] sizeof_void.c:16: User Error:
- sizeof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ sizeof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] sizeof_void.c:21: User Error:
- alignof on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ alignof on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] sizeof_void.c:28: User Error:
- alignof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ alignof() on void type only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] User Error: stopping on file "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 985351e9ac4efd6f3aef9393e0a6980017dfc493..5ed5a2552d7bdc8bf214e134b0f66d1bb4b00e55 100644
--- a/tests/value/oracle/array_zero_length.2.res.oracle
+++ b/tests/value/oracle/array_zero_length.2.res.oracle
@@ -1,16 +1,13 @@
[kernel] Parsing array_zero_length.i (no preprocessing)
[kernel] array_zero_length.i:9: User Error:
- zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] array_zero_length.i:11: User Error:
- zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] 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] array_zero_length.i:13: User Error:
- empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -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 446b635cc2cd1897e645b94688a5ece3a0e6bc81..019c09a82d65b2fb085b5c5523accd75088742c0 100644
--- a/tests/value/oracle/empty_base.1.res.oracle
+++ b/tests/value/oracle/empty_base.1.res.oracle
@@ -1,13 +1,10 @@
[kernel] Parsing empty_base.c (with preprocessing)
[kernel] empty_base.c:13: User Error:
- empty structs only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ empty structs only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] empty_base.c:48: User Error:
- zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ zero-length arrays only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps
[kernel] empty_base.c:50: User Error:
- empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or
- run '-machdep help' for the list of available machdeps
+ empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -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] = {{}};