From 3dfea57223cee736434d31d264b9fadaccd6ec26 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 12 Jan 2022 17:32:36 +0100
Subject: [PATCH] [Kernel] fix message about allowed machdeps
---
src/kernel_services/ast_queries/cil.ml | 4 ++--
tests/misc/oracle/function_ptr_alignof.res.oracle | 3 +--
tests/misc/oracle/function_ptr_sizeof.res.oracle | 3 +--
tests/syntax/oracle/compiler_builtins.0.res.oracle | 6 ++----
tests/syntax/oracle/compiler_builtins.1.res.oracle | 3 +--
tests/syntax/oracle/compiler_builtins.2.res.oracle | 9 +++------
.../oracle/flexible_array_member_invalid5.res.oracle | 3 +--
tests/syntax/oracle/sizeof_void.0.res.oracle | 12 ++++--------
tests/value/oracle/array_zero_length.2.res.oracle | 9 +++------
tests/value/oracle/empty_base.1.res.oracle | 9 +++------
10 files changed, 21 insertions(+), 40 deletions(-)
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index daae7bfac54..1b32804d971 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 fa223563fb4..c25dcf5f2d7 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 06996432c67..3f66d533ba6 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 6c6a5186dee..962db45f53c 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 0acfe18adc1..d3cf8ba1bb5 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 bdd362de663..cc838d9c9cd 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 8f91488188b..22cf6e91dad 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 03f35c1ead2..9ad43d07487 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 985351e9ac4..5ed5a2552d7 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 446b635cc2c..019c09a82d6 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] = {{}};
--
GitLab