diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 402bf50a070abbcb31fc98deefc04b330eeab1a5..77f6394a474424a899cac185a8d1b09f76b2ccf8 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -36,9 +36,11 @@ let pretty_cpp_opt_kind fmt =
type file =
| NeedCPP of
Filepath.Normalized.t (* filename of the [.c] to preprocess *)
- * string (* Preprocessor command.
- [filename.c -o tempfilname.i] will be appended at the
- end.*)
+ * string (* Preprocessing command, as given by -cpp-command, or
+ the default value, but without extra arguments *)
+ * string list (* Extra arguments to be given to the preprocessing
+ command, as given by -cpp-extra-args-per-file or
+ a JSON Compilation Database. *)
* cpp_opt_kind
| NoCPP of Filepath.Normalized.t (** filename of a preprocessed [.c] *)
| External of Filepath.Normalized.t * string
@@ -51,7 +53,7 @@ module D =
type t = file
let name = "File"
let reprs =
- [ NeedCPP(Filepath.Normalized.unknown, "", Unknown);
+ [ NeedCPP(Filepath.Normalized.unknown, "", [], Unknown);
NoCPP Filepath.Normalized.unknown;
External(Filepath.Normalized.unknown, "")
]
@@ -65,11 +67,12 @@ module D =
| External (f,p) ->
Format.fprintf fmt "@[File.External (%a,%S)@]"
Filepath.Normalized.pretty f p
- | NeedCPP (f,cmd,kind) ->
+ | NeedCPP (f,cmd,extra,kind) ->
Format.fprintf
- fmt "@[File.NeedCPP (%a,%S,%a)@]"
+ fmt "@[File.NeedCPP (%a,%S,%S,%a)@]"
Filepath.Normalized.pretty f
cmd
+ (String.concat " " extra)
pretty_cpp_opt_kind kind
in
Type.par p_caller Type.Call fmt pp
@@ -85,7 +88,7 @@ let get_suffixes () =
[ ".c"; ".i"; ".h" ]
let get_name s =
- let file = match s with NeedCPP (s,_,_) | NoCPP s | External (s,_) -> s in
+ let file = match s with NeedCPP (s,_,_,_) | NoCPP s | External (s,_) -> s in
Filepath.Normalized.to_pretty_string file
(* ************************************************************************* *)
@@ -118,24 +121,23 @@ let get_preprocessor_command () =
let from_filename ?cpp f =
let cpp =
- let cmdline = Kernel.CppCommand.get() in
- if cmdline <> "" then cmdline
- else
- let extra_by_file =
- try Kernel.CppExtraArgsPerFile.find f
- with Not_found -> ""
- in
- let jcdb_flags = Json_compilation_database.get_flags f in
- if extra_by_file <> "" && jcdb_flags <> [] then
- Kernel.warning ~wkey:Kernel.wkey_jcdb
- "found flags for file %a@ both in -cpp-extra-args-per-file and@ \
- in the json compilation database;@ the latter will be ignored"
- Filepath.Normalized.pretty f;
- let cpp =
- if cpp = None then get_preprocessor_command () else Option.get cpp
- in
- let flags = if extra_by_file <> "" then [extra_by_file] else jcdb_flags in
- String.concat " " (cpp :: flags)
+ let cpp_command = Kernel.CppCommand.get() in
+ if cpp_command <> "" then cpp_command
+ else if cpp = None then get_preprocessor_command ()
+ else Option.get cpp
+ in
+ let extra =
+ let extra_by_file =
+ try Kernel.CppExtraArgsPerFile.find f
+ with Not_found -> ""
+ in
+ let jcdb_flags = Json_compilation_database.get_flags f in
+ if extra_by_file <> "" && jcdb_flags <> [] then
+ Kernel.warning ~wkey:Kernel.wkey_jcdb
+ "found flags for file %a@ both in -cpp-extra-args-per-file and@ \
+ in the json compilation database;@ the latter will be ignored"
+ Filepath.Normalized.pretty f;
+ if extra_by_file <> "" then [extra_by_file] else jcdb_flags
in
if Filename.check_suffix (f:>string) ".i" then begin
NoCPP f
@@ -154,7 +156,7 @@ let from_filename ?cpp f =
Kernel.warning ~once:true
"Default pre-processor does not keep comments. Any ACSL annotation \
on non-pre-processed file will be discarded.";
- NeedCPP (f, cpp, is_cpp_gnu_like ())
+ NeedCPP (f, cpp, extra, is_cpp_gnu_like ())
end else
Kernel.abort "No working pre-processor found. You can only analyze \
pre-processed .i files."
@@ -440,7 +442,7 @@ let concat_strs ?(pre="") ?(sep=" ") l =
let build_cpp_cmd = function
| NoCPP _ | External _ -> None
- | NeedCPP (f, cmdl, is_gnu_like) ->
+ | NeedCPP (f, cmdl, extra, is_gnu_like) ->
if not (Sys.file_exists (f :> string)) then
Kernel.abort "source file %a does not exist"
Filepath.Normalized.pretty f;
@@ -519,16 +521,16 @@ let build_cpp_cmd = function
in
let supp_args =
string_of_supp_args
- (Kernel.CppExtraArgs.get () @ gnu_implicit_args @ supported_cpp_arch_args)
+ (Kernel.CppExtraArgs.get () @ gnu_implicit_args @ supported_cpp_arch_args @ extra)
include_args define_args
in
let cpp_command = replace_in_cpp_cmd cmdl supp_args (f:>string) (ppf:>string) in
Kernel.feedback ~dkey:Kernel.dkey_pp
"@{<i>preprocessing@} with \"%s\""
cpp_command;
- Some (cpp_command, ppf, supported_cpp_arch_args)
+ Some (cpp_command, ppf, supp_args)
-let parse_cabs cpp_command_no_output = function
+let parse_cabs cpp_command = function
| NoCPP f ->
if not (Sys.file_exists (f:>string)) then
Kernel.abort "preprocessed file %a does not exist"
@@ -536,8 +538,8 @@ let parse_cabs cpp_command_no_output = function
Kernel.feedback "Parsing %a (no preprocessing)"
Datatype.Filepath.pretty f;
Frontc.parse f ()
- | NeedCPP (f, cmdl, is_gnu_like) ->
- let cpp_command, ppf, supported_cpp_arch_args = Option.get cpp_command_no_output in
+ | NeedCPP (f, cmdl, _extra, is_gnu_like) ->
+ let cpp_command, ppf, supp_args = Option.get cpp_command in
Kernel.feedback "Parsing %a (with preprocessing)"
Datatype.Filepath.pretty f;
if Sys.command cpp_command <> 0 then begin
@@ -581,13 +583,9 @@ let parse_cabs cpp_command_no_output = function
"trying to preprocess annotation with an unknown \
preprocessor."; true))
then begin
- let pp_annot_supp_args =
- Format.asprintf "-nostdinc %s"
- (concat_strs supported_cpp_arch_args)
- in
let ppf' =
try Logic_preprocess.file ".c"
- (replace_in_cpp_cmd cmdl pp_annot_supp_args)
+ (replace_in_cpp_cmd cmdl supp_args)
(ppf : Filepath.Normalized.t :> string)
with Sys_error _ as e ->
safe_remove_file ppf;
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 979ee3d7721c834f9ca225eb581cd408a6a4a8f8..5cbfef57263eb571b3967497ca1e6fbbae8b8a3a 100644
--- a/src/kernel_services/ast_queries/file.mli
+++ b/src/kernel_services/ast_queries/file.mli
@@ -30,10 +30,14 @@ type cpp_opt_kind = Gnu | Not_gnu | Unknown
Note: [string] is used here instead of [Filepath], to preserve
names given on the command line, without normalization. *)
type file =
- | NeedCPP of Filepath.Normalized.t * string * cpp_opt_kind
- (** The first string is the filename of the [.c] to preprocess.
- The second one is the preprocessor command ([filename.c -o
- tempfilname.i] will be appended at the end).*)
+ | NeedCPP of Filepath.Normalized.t * string * string list * cpp_opt_kind
+ (** File which needs preprocessing.
+ NeedCPP(filepath, cmd, extra, cpp_opt_kind):
+ - filepath: source file to be preprocessed;
+ - cmd: preprocessing command, before replacement of '%'-arguments;
+ - extra: list of extra arguments (e.g. from a JCDB);
+ - cpp_opt_kind: whether the preprocessor supports GNU options
+ such as -I/-D. *)
| NoCPP of Filepath.Normalized.t
(** Already pre-processed file [.i] *)
| External of Filepath.Normalized.t * string
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index f2389fe2e8ada1276a640ceb2689b7ff4f5a6f76..caf9e83a15294ec38baa1aec35760c73ecbcd5c9 100644
--- a/tests/jcdb/jcdb.c
+++ b/tests/jcdb/jcdb.c
@@ -4,6 +4,7 @@ OPT: -json-compilation-database @PTEST_DIR@ -print
OPT: @PTEST_DIR@/jcdb2.c -json-compilation-database @PTEST_DIR@/with_arguments.json -print
OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
+EXECNOW: LOG logic-pp-include.res LOG logic-pp-include.err @frama-c@ -json-compilation-database @PTEST_DIR@/logic-pp-include @PTEST_DIR@/logic-pp-include/no-stdio.c -print -no-autoload-plugins > @PTEST_DIR@/result/logic-pp-include.res 2> @PTEST_DIR@/result/logic-pp-include.err
*/
#include <stdio.h>
diff --git a/tests/jcdb/logic-pp-include/compile_commands.json b/tests/jcdb/logic-pp-include/compile_commands.json
new file mode 100644
index 0000000000000000000000000000000000000000..9e4246444d3e953299c8e11a2716c4d678b88369
--- /dev/null
+++ b/tests/jcdb/logic-pp-include/compile_commands.json
@@ -0,0 +1,11 @@
+[
+ {
+ "arguments": [
+ "-include",
+ "stdio.h",
+ "-DZERO=0"
+ ],
+ "directory": ".",
+ "file": "no-stdio.c"
+ }
+]
diff --git a/tests/jcdb/logic-pp-include/no-stdio.c b/tests/jcdb/logic-pp-include/no-stdio.c
new file mode 100644
index 0000000000000000000000000000000000000000..78444816bb2ae859c54f7156033ff7df90c39aa0
--- /dev/null
+++ b/tests/jcdb/logic-pp-include/no-stdio.c
@@ -0,0 +1,5 @@
+// compile_commands.json must have "-includestdio.h" and define ZERO
+int main(){
+ printf("bla\n");
+ return ZERO;
+}
diff --git a/tests/jcdb/oracle/logic-pp-include.err b/tests/jcdb/oracle/logic-pp-include.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/jcdb/oracle/logic-pp-include.res b/tests/jcdb/oracle/logic-pp-include.res
new file mode 100644
index 0000000000000000000000000000000000000000..a6aedf5c3dda4ac6f804a2708246461654bef1c8
--- /dev/null
+++ b/tests/jcdb/oracle/logic-pp-include.res
@@ -0,0 +1,15 @@
+[kernel] Parsing tests/jcdb/logic-pp-include/no-stdio.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+int main(void)
+{
+ int __retres;
+ printf("bla\n");
+ __retres = 0;
+ return __retres;
+}
+
+