From 4a19d4b771298abcfcb8829c8b1b5a51976857c0 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 4 Jan 2023 18:58:22 +0100
Subject: [PATCH] [Kernel] improve warning messages
---
src/kernel_services/ast_queries/file.ml | 10 +++++-----
tests/spec/oracle/preprocess_string.res.oracle | 2 +-
tests/syntax/oracle/cpp-command.6.res.oracle | 4 ++--
3 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index d029891d4a2..a607b34e6d1 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -132,12 +132,12 @@ let from_filename ?cpp f =
else if cpp <> "" then begin
if not Fc_config.preprocessor_keep_comments then
Kernel.warning ~once:true
- "Default pre-processor does not keep comments. Any ACSL annotation \
- on non-pre-processed file will be discarded.";
+ "Default preprocessor does not keep comments. Any ACSL annotations \
+ on non-preprocessed files will be discarded.";
NeedCPP (f, cpp, extra_for_this_file, is_cpp_gnu_like ())
end else
- Kernel.abort "No working pre-processor found. You can only analyze \
- pre-processed .i files."
+ Kernel.abort "No working preprocessor found. You can only analyze \
+ preprocessed .i files."
(* ************************************************************************* *)
(** {2 Internal states} *)
@@ -501,7 +501,7 @@ let build_cpp_cmd = function
Kernel.warning
~once:true
"your preprocessor is not known to handle option `%s'. \
- If pre-processing fails because of it, please add \
+ If preprocessing fails because of it, please add \
-no-cpp-frama-c-compliant option to Frama-C's command-line. \
If you do not want to see this warning again, explicitly use \
option -cpp-frama-c-compliant."
diff --git a/tests/spec/oracle/preprocess_string.res.oracle b/tests/spec/oracle/preprocess_string.res.oracle
index f7ee475466e..ea37c11725b 100644
--- a/tests/spec/oracle/preprocess_string.res.oracle
+++ b/tests/spec/oracle/preprocess_string.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
+[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Parsing preprocess_string.c (with preprocessing)
/* Generated by Frama-C */
/*@ ensures *("/*" + 0) ≡ '/'; */
diff --git a/tests/syntax/oracle/cpp-command.6.res.oracle b/tests/syntax/oracle/cpp-command.6.res.oracle
index ef44555760e..f59eb94c447 100644
--- a/tests/syntax/oracle/cpp-command.6.res.oracle
+++ b/tests/syntax/oracle/cpp-command.6.res.oracle
@@ -1,5 +1,5 @@
-[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
-[kernel] Warning: your preprocessor is not known to handle option `-dD'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
+[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
+[kernel] Warning: your preprocessor is not known to handle option `-dD'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Parsing cpp-command.c (with preprocessing)
extra_args: -ITMP_MACHDEP -IFRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc file_extra global_extra
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
--
GitLab