From 8bcef50f1d9047d4d93b9133b847f0647dfa967d Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 1 Jul 2020 21:43:08 +0200
Subject: [PATCH] [Kernel] improve error message when preprocessing fails
---
src/kernel_services/ast_queries/file.ml | 26 +++++++--
.../ast_queries/json_compilation_database.ml | 53 ++++++++++---------
.../ast_queries/json_compilation_database.mli | 6 +++
3 files changed, 58 insertions(+), 27 deletions(-)
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 412c9452930..6deba7d75d1 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -533,11 +533,31 @@ let parse_cabs = function
let cpp_command = build_cpp_cmd cmdl supp_args (f:>string) (ppf:>string) in
if Sys.command cpp_command <> 0 then begin
safe_remove_file ppf;
+ let possible_cause =
+ if Kernel.JsonCompilationDatabase.is_set () then
+ if not (Json_compilation_database.has_entry f) then
+ Format.asprintf "note: %s is set but \
+ contains no entries for '%a'.@ "
+ Kernel.JsonCompilationDatabase.option_name
+ Datatype.Filepath.pretty f
+ else ""
+ else
+ if not (Kernel.CppExtraArgs.is_set ()) &&
+ not (Kernel.CppExtraArgsPerFile.is_set ()) &&
+ not (Kernel.CppCommand.is_set ()) then
+ Format.asprintf
+ "this is possibly due to missing preprocessor flags;@ \
+ consider options %s, %s or %s.@ "
+ Kernel.CppExtraArgs.option_name
+ Kernel.JsonCompilationDatabase.option_name
+ Kernel.CppCommand.option_name
+ else ""
+ in
Kernel.abort
"failed to run: %s@\n\
- you may set the CPP environment variable to select the proper \
- preprocessor command or use the option \"-cpp-command\"."
- cpp_command
+ %sSee chapter \"Preparing the Sources\" in the Frama-C user manual \
+ for more details."
+ cpp_command possible_cause
end;
let ppf =
if Kernel.ReadAnnot.get() &&
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ml b/src/kernel_services/ast_queries/json_compilation_database.ml
index 091216de519..5e0124ac2b1 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ml
@@ -239,32 +239,33 @@ let parse_entry jcdb_dir r =
| Not_found ->
Flags.add path flags
+let compute_flags_from_file () =
+ let database = Kernel.JsonCompilationDatabase.get () in
+ let jcdb_dir, jcdb_path =
+ if Sys.is_directory database then
+ database, Filename.concat database "compile_commands.json"
+ else Filename.dirname database, database
+ in
+ Kernel.feedback ~dkey:Kernel.dkey_compilation_db
+ "using compilation database: %s" jcdb_path;
+ begin
+ try
+ let r_list =
+ Yojson.Basic.from_file jcdb_path |> Yojson.Basic.Util.to_list
+ in
+ List.iter (parse_entry jcdb_dir) r_list;
+ with
+ | Sys_error msg
+ | Yojson.Json_error msg
+ | Yojson.Basic.Util.Type_error (msg, _) ->
+ Kernel.abort "could not parse compilation database: %s@ %s"
+ database msg
+ end;
+ Flags.mark_as_computed ()
+
let get_flags f =
if Kernel.JsonCompilationDatabase.get () <> "" then begin
- if not (Flags.is_computed ()) then begin
- let database = Kernel.JsonCompilationDatabase.get () in
- let jcdb_dir, jcdb_path =
- if Sys.is_directory database then
- database, Filename.concat database "compile_commands.json"
- else Filename.dirname database, database
- in
- Kernel.feedback ~dkey:Kernel.dkey_compilation_db
- "using compilation database: %s" jcdb_path;
- begin
- try
- let r_list =
- Yojson.Basic.from_file jcdb_path |> Yojson.Basic.Util.to_list
- in
- List.iter (parse_entry jcdb_dir) r_list;
- with
- | Sys_error msg
- | Yojson.Json_error msg
- | Yojson.Basic.Util.Type_error (msg, _) ->
- Kernel.abort "could not parse compilation database: %s@ %s"
- database msg
- end;
- Flags.mark_as_computed ()
- end;
+ if not (Flags.is_computed ()) then compute_flags_from_file ();
try
let flags = Flags.find f in
Kernel.feedback ~dkey:Kernel.dkey_compilation_db
@@ -276,3 +277,7 @@ let get_flags f =
[]
end
else []
+
+let has_entry f =
+ if not (Flags.is_computed ()) then compute_flags_from_file ();
+ Flags.mem f
diff --git a/src/kernel_services/ast_queries/json_compilation_database.mli b/src/kernel_services/ast_queries/json_compilation_database.mli
index 9e3101b1d8a..5b9f18f1b08 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.mli
+++ b/src/kernel_services/ast_queries/json_compilation_database.mli
@@ -24,3 +24,9 @@
in the JSON compilation database (when enabled), or the empty string
otherwise. If not empty, the flags always start with a space. *)
val get_flags : Datatype.Filepath.t -> string list
+
+(** [has_entry f] returns true iff [f] has an entry in the JSON compilation
+ database. Must only be called if a JCDB file has been specified.
+ @since Frama-C+dev
+*)
+val has_entry : Datatype.Filepath.t -> bool
--
GitLab