From a480d4bf4f745f8940309666fbc6d8a37c64ae04 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Wed, 4 Mar 2020 19:11:32 +0100
Subject: [PATCH] [Kernel] add option -cpp-extra-args-per-file
---
doc/userman/user-changes.tex | 5 +++
doc/userman/user-sources.tex | 2 ++
man/frama-c.1 | 8 ++++-
man/frama-c.1.header | 2 +-
man/frama-c.1.md | 4 +++
src/kernel_services/ast_queries/file.ml | 13 ++++++-
.../cmdline_parameters/parameter_builder.ml | 24 +++++++++++++
.../cmdline_parameters/parameter_sig.mli | 16 +++++++++
.../plugin_entry_points/kernel.ml | 34 +++++++++++++++++++
.../plugin_entry_points/kernel.mli | 3 ++
tests/misc/cpp-extra-args-per-file1.c | 20 +++++++++++
tests/misc/cpp-extra-args-per-file2.c | 15 ++++++++
.../cpp-extra-args-per-file1.res.oracle | 2 ++
13 files changed, 145 insertions(+), 3 deletions(-)
create mode 100644 tests/misc/cpp-extra-args-per-file1.c
create mode 100644 tests/misc/cpp-extra-args-per-file2.c
create mode 100644 tests/misc/oracle/cpp-extra-args-per-file1.res.oracle
diff --git a/doc/userman/user-changes.tex b/doc/userman/user-changes.tex
index e9e0c934891..75f767128b9 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 8fc0e1180af..cba9cf513df 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 0d19ee714ab..706d54135e1 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 367a0c8bd4b..ce56197c3e9 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 7e21eccfa57..c5835e67eb2 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 99008be9f27..0267c03d381 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 fc7cf42a98c..74ab79bec5a 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 0f0e7ecc920..060ea584248 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 cce382d5d4e..7ed97572321 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 bbfdc8097ff..8a371085fbd 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 00000000000..49f13a4f541
--- /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 00000000000..baa99d93c02
--- /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 00000000000..d32c7d2d184
--- /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)
--
GitLab