diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 0d0b2949cf04b95003c0fd38891e45d4e700d069..30ebd9bdf6278c11feb8177967ff91a742801a0a 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -119,7 +119,7 @@ let from_filename ?cpp f =
| None -> get_preprocessor_command ()
| Some cpp -> cpp, cpp_opt_kind ()
in
- (if flags = "" then cpp else cpp ^ " " ^ flags), gnu
+ (if flags = [] then cpp else cpp ^ " " ^ String.concat " " flags), gnu
in
if Filename.check_suffix f ".i" then begin
NoCPP f
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ko.ml b/src/kernel_services/ast_queries/json_compilation_database.ko.ml
index 414499c6ddacb0ff22e34a9c94ccf0f4aff3d762..646e41872a63bee993e9bb52fe70bfed2e46124c 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ko.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ko.ml
@@ -31,4 +31,4 @@ let get_flags _ =
"Attempt to parse json compilation database %s \
with a Frama-C compiled without Yojson support." db
end;
- ""
+ []
diff --git a/src/kernel_services/ast_queries/json_compilation_database.mli b/src/kernel_services/ast_queries/json_compilation_database.mli
index f343d4a1f4cc8aed52019ce213ee41ca5b8e0b40..dcb18cb059b83c2c32da10c78f34e6081fc3018f 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.mli
+++ b/src/kernel_services/ast_queries/json_compilation_database.mli
@@ -23,4 +23,4 @@
(** [get_flags f] returns the preprocessing flags associated to file [f]
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
+val get_flags : Datatype.Filepath.t -> string list
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ok.ml b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
index 6ae9e02ee25d6cdd5f5b409eebf0acedb0d45063..6409629514e1ef8bc06823880b27aeb49ac5e2a2 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ok.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
@@ -20,10 +20,12 @@
(* *)
(**************************************************************************)
+module StringList = Datatype.List(Datatype.String)
+
module Flags =
State_builder.Hashtbl
(Datatype.Filepath.Hashtbl)
- (Datatype.String)
+ (StringList)
(struct
let name ="JsonCompilationDatabase.Flags"
let dependencies = [Kernel.JsonCompilationDatabase.self]
@@ -205,18 +207,28 @@ let parse_entry ?(cwd=Sys.getcwd()) (r : Yojson.Basic.json) =
(* Note: the same file may be compiled several times, under different
(and possibly incompatible) configurations, leading to multiple
occurrences in the list. Since we cannot infer which of them is the
- "right" one, we pick the first and warn the user if there are
- others. *)
- let flags = String.concat " " (List.rev res) in
+ "right" one, we replace them with the latest ones found, warning the
+ user if previous flags were different. *)
+ let flags = List.rev res in
try
let previous_flags = Flags.find path in
if previous_flags <> flags then
+ let removed_flags = List.filter (fun e -> not (List.mem e previous_flags)) flags in
+ let removed_str =
+ if removed_flags = [] then "" else
+ Format.asprintf "@ Old flags no longer present: %a"
+ (Pretty_utils.pp_list ~sep:" " Format.pp_print_string) removed_flags
+ in
+ let added_flags = List.filter (fun e -> not (List.mem e flags)) previous_flags in
+ let added_str =
+ if added_flags = [] then "" else
+ Format.asprintf "@ New flags not previously present: %a"
+ (Pretty_utils.pp_list ~sep:" " Format.pp_print_string) added_flags
+ in
Kernel.warning ~wkey:Kernel.wkey_jcdb
- "@[<v>found duplicate flags for '%a'.\
- @ Previous flags: %s\
- @ New flags: %s@]" Datatype.Filepath.pretty path
- previous_flags flags;
- Flags.replace path flags
+ "@[<v>found duplicate flags for '%a', replacing old flags.%s%s@]"
+ Datatype.Filepath.pretty path removed_str added_str;
+ Flags.replace path flags
with
| Not_found ->
Flags.add path flags
@@ -250,11 +262,11 @@ let get_flags f =
try
let flags = Flags.find f in
Kernel.feedback ~dkey:Kernel.dkey_compilation_db
- "flags found for '%a': %s" Datatype.Filepath.pretty f flags;
+ "flags found for '%a': %a" Datatype.Filepath.pretty f StringList.pretty flags;
flags
with Not_found ->
Kernel.feedback ~dkey:Kernel.dkey_compilation_db
"no flags found for '%a'" Datatype.Filepath.pretty f;
- ""
+ []
end
- else ""
+ else []
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 4edd4171dfd05aa954861ef917289330a993592b..7d55bd3c1554bb170fd9a12d57f23a406d595a88 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -153,6 +153,7 @@ let () = set_warn_status wkey_cert_exp_10 Log.Winactive
let wkey_check_volatile = register_warn_category "check:volatile"
let wkey_jcdb = register_warn_category "pp:compilation-db"
+let () = set_warn_status wkey_jcdb Log.Wonce
let wkey_implicit_function_declaration = register_warn_category
"typing:implicit-function-declaration"
diff --git a/tests/jcdb/oracle/jcdb.0.res.oracle b/tests/jcdb/oracle/jcdb.0.res.oracle
index fc6e678e7541aa6336f91a8044e67d6ac8a685c6..1a80090d55b0c602628524a47fa26ba90e0cf493 100644
--- a/tests/jcdb/oracle/jcdb.0.res.oracle
+++ b/tests/jcdb/oracle/jcdb.0.res.oracle
@@ -1,7 +1,8 @@
[kernel:pp:compilation-db] Warning:
- found duplicate flags for 'tests/jcdb/jcdb.c'.
- Previous flags: -DDUPLICATE_FLAGS_THAT_WILL_BE_OVERWRITTEN
- New flags: -D'MSG="a \" \"b"' -D'SINGLE_DOUBLE(a)="a \"with spaces and tab "' -DSOMEDEF="With spaces, quotes and \-es." -D"DOUBLE_SINGLE(a)=a \"macro with spaces and non-escaped \\'\"" -DEMPTY='' -DEMPTY2= -DTEST=42 -D'MACRO_FOR_INCR(s)=s+1' -DTOUNDEF -UTOUNDEF
+ found duplicate flags for 'tests/jcdb/jcdb.c', replacing old flags.
+ Old flags no longer present: -D'MSG="a \" \"b"' -D'SINGLE_DOUBLE(a)="a \"with spaces and tab "' -DSOMEDEF="With spaces, quotes and \-es." -D"DOUBLE_SINGLE(a)=a \"macro with spaces and non-escaped \\'\"" -DEMPTY='' -DEMPTY2= -DTEST=42 -D'MACRO_FOR_INCR(s)=s+1' -DTOUNDEF -UTOUNDEF
+ New flags not previously present: -DDUPLICATE_FLAGS_THAT_WILL_BE_OVERWRITTEN
+ (warn-once: no further messages from category 'pp:compilation-db' will be emitted)
[kernel] Parsing tests/jcdb/jcdb.c (with preprocessing)
/* Generated by Frama-C */
#include "errno.h"