diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index e9e0c934891bf2a5a372d44cff3d823608d2d038..75f767128b9a43f7c8fcb74845682e116f525124 100644
--- a/doc/userman/user-changes.tex
+++ b/doc/userman/user-changes.tex
@@ -5,6 +5,11 @@ release. First we list changes of the last release.
\section*{\nextframacversion}
+\begin{itemize}
+\item \textbf{Preparing the Sources:} added option
+ \texttt{-cpp-extra-args-per-file}.
+\end{itemize}
+
\section*{20.0 (Calcium)}
\begin{itemize}
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index 8fc0e1180af15d70df8d4e32022b3a26e3597857..cba9cf513df62a245bce9103ab288d7959d194a0 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -59,6 +59,8 @@ allows the user to extend the pre-processing command,
typically via the inclusion of defines (\texttt{-D} switches) and header
directories (\texttt{-I} switches), as in
\texttt{-cpp-extra-args="-DDEBUG -DARCH=ia32 -I./headers"}.
+You can also add arguments on a per-file basis, using option
+\optiondef{-}{cpp-extra-args-per-file}.
If you have a JSON compilation database file\footnote{%
\url{http://clang.llvm.org/docs/JSONCompilationDatabase.html}}, you can use
diff --git a/man/frama-c.1 b/man/frama-c.1
index 0d19ee714abd6bd0e28a0224e638a1ff2763c1ac..706d54135e1785b604e998aaccc3522b72559ceb 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -25,7 +25,7 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2019-07-29
+.TH FRAMA-C 1 2020-03-05
.SH NAME
.PP
frama\-c[.byte] \- a static analyzer for C programs
@@ -262,6 +262,12 @@ definitions) must thus go there instead of \f[B]\-cpp\-command\f[].
.RS
.RE
.TP
+.B \-cpp\-extra\-args\-per\-file \f[I]file1:args1,\&...,filen:argsn\f[]
+like \f[B]\-cpp\-extra\-args\f[], but the arguments only apply to the
+specified files.
+.RS
+.RE
+.TP
.B [\-no]\-cpp\-frama\-c\-compliant
indicates that the chosen preprocessor complies to some Frama\-C
requirements, such as accepting the same set of options as GNU cpp, and
diff --git a/man/frama-c.1.header b/man/frama-c.1.header
index 367a0c8bd4b193406919e0c0e0dd58fbc482dea2..ce56197c3e948b460514eedb2979d4a8b162ebe7 100644
--- a/man/frama-c.1.header
+++ b/man/frama-c.1.header
@@ -25,4 +25,4 @@
.\" using pandoc 2.0 or newer. To modify this file, edit the Markdown file
.\" and run `make man/frama-c.1`.
-.TH FRAMA-C 1 2019-07-29
+.TH FRAMA-C 1 2020-03-05
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 7e21eccfa57736ffd7be6ef615dfeb6f1a0e11e4..c5835e67eb2679f7bd0c620019070b21d54f4761 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -156,6 +156,10 @@ pre-processed. *args* are used only for the first pass, so that arguments that
should not be used twice (such as additional include directives or macro
definitions) must thus go there instead of **-cpp-command**.
+-cpp-extra-args-per-file *file1:args1,...,filen:argsn*
+: like **-cpp-extra-args**, but the arguments only apply to the specified
+files.
+
[-no]-cpp-frama-c-compliant
: indicates that the chosen preprocessor complies to some Frama-C requirements,
such as accepting the same set of options as GNU cpp, and accepting
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 99008be9f2759e59c0896a7f742b8fc4e5175948..0267c03d3815f23e58bf7bd98f477bd8fd61b6c5 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -123,12 +123,22 @@ let from_filename ?cpp f =
if cmdline <> "" then
cmdline, cpp_opt_kind ()
else
- let flags = Json_compilation_database.get_flags f in
+ let jcdb_flags = Json_compilation_database.get_flags f in
let cpp, gnu =
match cpp with
| None -> get_preprocessor_command ()
| Some cpp -> cpp, cpp_opt_kind ()
in
+ let extra_flags =
+ try Kernel.CppExtraArgsPerFile.find f
+ with Not_found -> ""
+ in
+ if jcdb_flags <> [] && extra_flags <> "" then
+ Kernel.warning ~once:true
+ "found flags for file %a both in json compilation database and \
+ -cpp-extra-args-per-file; this is unsupported and non-deterministic \
+ behavior may happen" Filepath.Normalized.pretty f;
+ let flags = extra_flags :: jcdb_flags in
(if flags = [] then cpp else cpp ^ " " ^ String.concat " " flags), gnu
in
if Filename.check_suffix (f:>string) ".i" then begin
@@ -173,6 +183,7 @@ end = struct
let dependencies =
[ Kernel.CppCommand.self;
Kernel.CppExtraArgs.self;
+ Kernel.CppExtraArgsPerFile.self;
Kernel.JsonCompilationDatabase.self;
Kernel.Files.self ]
let name = "Files for preprocessing"
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index fc7cf42a98cfaccda4067f4f6b0b732c072e0074..74ab79bec5a85eca6ed379d42c920b271409b659 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -1418,6 +1418,30 @@ struct
(V)
(struct include X let dependencies = [] end)
+ module Filepath_map
+ (V: Parameter_sig.Value_datatype with type key = Fc_Filepath.Normalized.t)
+ (X: sig
+ include Parameter_sig.Input_with_arg
+ val existence: Fc_Filepath.existence
+ val default: V.t Datatype.Filepath.Map.t
+ end) =
+ Make_map
+ (struct
+ include Datatype.Filepath
+ let of_string s =
+ try
+ Fc_Filepath.Normalized.of_string ~existence:X.existence s
+ with
+ | Fc_Filepath.No_file ->
+ P.L.abort "file '%s' not found" s
+ | Fc_Filepath.File_exists ->
+ P.L.abort "file '%s' already exists" s
+ let to_string = Fc_Filepath.Normalized.to_pretty_string
+ let of_singleton_string = no_element_of_string
+ end)
+ (V)
+ (struct include X let dependencies = [] end)
+
module Kernel_function_map
(V: Parameter_sig.Value_datatype with type key = kernel_function)
(X: sig
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 0f0e7ecc920167495d9f83570cf6fc35b267da79..060ea5842489ddacd0c62b317e5f6ad4852c9880 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -482,6 +482,9 @@ module type Multiple_map = sig
val mem: key -> bool
end
+module type Filepath_map =
+ Map with type key = Datatype.Filepath.t
+
(* ************************************************************************** *)
(** {2 All the different kinds of command line options as functors} *)
(* ************************************************************************** *)
@@ -573,6 +576,19 @@ module type Builder = sig
(** see [Filepath] module. *)
end): Filepath_list
+ module Filepath_map
+ (V: Value_datatype with type key = Fc_Filepath.Normalized.t)
+ (X: sig
+ include Input_with_arg
+ val default: V.t Datatype.Filepath.Map.t
+ val existence: Fc_Filepath.existence
+ val file_kind: string
+ end):
+ Map
+ with type key = Fc_Filepath.Normalized.t
+ and type value = V.t
+ and type t = V.t Datatype.Filepath.Map.t
+
(** Parameter is a map where multibindings are **not** allowed. *)
module Make_map
(K: String_datatype_with_collections)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index cce382d5d4e14eb6c2f28d6bd0c2b66bbce7dcbb..7ed97572321d668bdf3dc46f882742d4d1ac8740 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -263,6 +263,25 @@ module Filepath_list
include X
end)
+module Filepath_map
+ (X: sig
+ include Input_with_arg
+ val existence: Filepath.existence
+ val file_kind: string
+ end) =
+ P.Filepath_map
+ (struct
+ include Datatype.String
+ type key = Filepath.Normalized.t
+ let of_string ~key:_ ~prev:_ s = s
+ let to_string ~key:_ s = s
+ end)
+ (struct
+ let () = Parameter_customize.set_module_name X.module_name
+ include X
+ let default = Datatype.Filepath.Map.empty
+ end)
+
module Kernel_function_set(X: Input_with_arg) =
P.Kernel_function_set
(struct
@@ -924,6 +943,21 @@ module CppExtraArgs =
preprocessing the C code but not while preprocessing annotations"
end)
+let () = Parameter_customize.set_group parsing
+let () = Parameter_customize.do_not_reset_on_copy ()
+module CppExtraArgsPerFile =
+ Filepath_map
+ (struct
+ let module_name = "CppExtraArgsPerFile"
+ let option_name = "-cpp-extra-args-per-file"
+ let arg_name = "file:flags"
+ let existence = Filepath.Must_exist
+ let file_kind = "source"
+ let help =
+ "when set, adds preprocessing arguments for each specified file. \
+ To add arguments for all files, use -cpp-extra-args."
+ end)
+
let () = Parameter_customize.set_group parsing
let () = Parameter_customize.do_not_reset_on_copy ()
module CppGnuLike =
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index bbfdc8097ff04f6d3412874c6a574ad853a1d5c4..8a371085fbdda7f9eb1f046a87770ad92624a757 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -378,6 +378,9 @@ module CppCommand: Parameter_sig.String
module CppExtraArgs: Parameter_sig.String_list
(** Behavior of option "-cpp-extra-args" *)
+module CppExtraArgsPerFile: Parameter_sig.Filepath_map with type value = string
+(** Behavior of option "-cpp-extra-args-per-file" *)
+
module CppGnuLike: Parameter_sig.Bool
(** Behavior of option "-cpp-frama-c-compliant" *)
diff --git a/tests/misc/cpp-extra-args-per-file1.c b/tests/misc/cpp-extra-args-per-file1.c
new file mode 100644
index 0000000000000000000000000000000000000000..49f13a4f541a8022ed293889ee7dd15633e598ab
--- /dev/null
+++ b/tests/misc/cpp-extra-args-per-file1.c
@@ -0,0 +1,20 @@
+/* run.config
+ OPT: -no-autoload-plugins -cpp-extra-args="-DGLOBAL" -cpp-extra-args-per-file @PTEST_DIR@/cpp-extra-args-per-file1.c:'-DFILE1 -DMACRO_WITH_QUOTES="\"hello world"\"',@PTEST_DIR@/cpp-extra-args-per-file2.c:"-DFILE2" -then @PTEST_DIR@/cpp-extra-args-per-file2.c
+ */
+
+#ifndef GLOBAL
+#error GLOBAL must be defined
+#endif
+
+#ifndef FILE1
+#error FILE1 must be defined
+#endif
+
+#ifdef FILE2
+#error FILE2 must NOT be defined
+#endif
+
+int main() {
+ char *a = MACRO_WITH_QUOTES;
+ return 0;
+}
diff --git a/tests/misc/cpp-extra-args-per-file2.c b/tests/misc/cpp-extra-args-per-file2.c
new file mode 100644
index 0000000000000000000000000000000000000000..baa99d93c02e6c4e64b14e63e4e3ca6759dce261
--- /dev/null
+++ b/tests/misc/cpp-extra-args-per-file2.c
@@ -0,0 +1,15 @@
+/* run.config
+ DONTRUN: main test is cpp-extra-args-per-file1.c
+ */
+
+#ifndef GLOBAL
+#error GLOBAL must be defined
+#endif
+
+#ifndef FILE2
+#error FILE2 must be defined
+#endif
+
+#ifdef FILE1
+#error FILE1 must NOT be defined
+#endif
diff --git a/tests/misc/oracle/cpp-extra-args-per-file1.res.oracle b/tests/misc/oracle/cpp-extra-args-per-file1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d32c7d2d1848f505fd70cd86f11e95d5c02490ae
--- /dev/null
+++ b/tests/misc/oracle/cpp-extra-args-per-file1.res.oracle
@@ -0,0 +1,2 @@
+[kernel] Parsing tests/misc/cpp-extra-args-per-file1.c (with preprocessing)
+[kernel] Parsing tests/misc/cpp-extra-args-per-file2.c (with preprocessing)