diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 412c945293053724d86025b26b3ebab33b0905ce..6deba7d75d1e529660d1516ff905088ba8af6f8d 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 091216de519479409665cb4a4cb5bf1f27a94a8d..5e0124ac2b1d59fb49d71896598f905243a8cec7 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 9e3101b1d8a2ead1ee26330ee039c88749c0dbee..5b9f18f1b087c5dc1b185eb10404de4584f0f49d 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