diff --git a/src/kernel_internals/parsing/logic_preprocess.mll b/src/kernel_internals/parsing/logic_preprocess.mll
index 765d158daf4a966e8c609f7a6f0e56426b143a7e..1db7292b1f288a267f3c2560164c45440b179441 100644
--- a/src/kernel_internals/parsing/logic_preprocess.mll
+++ b/src/kernel_internals/parsing/logic_preprocess.mll
@@ -171,7 +171,10 @@
       Buffer.output_buffer ppfile preprocess_buffer;
       close_out ppfile;
       let cppname = Extlib.temp_file_cleanup_at_exit ~debug "cppannot" suffix in
-      let res = Sys.command (cpp ppname cppname) in
+      let pp_cmd = cpp ppname cppname in
+      Kernel.feedback ~dkey:Kernel.dkey_pp_logic
+        "logic preprocessing with \"%s\"" pp_cmd;
+      let res = Sys.command pp_cmd in
       let result_file =
         if res <> 0 then begin
           abort_preprocess "Preprocessor call exited with an error";
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index bf305b358d728b3abdf4148586ccb989287efb7c..198d03db923ff73c738c8f593d2471acba92aab4 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
 
 (* ************************************************************************* *)
@@ -99,6 +102,14 @@ let cpp_opt_kind () =
     if Kernel.CppGnuLike.get () then Gnu else Not_gnu
   else Unknown
 
+let is_cpp_gnu_like () =
+  let open Fc_config in
+  let cpp_cmd = Kernel.CppCommand.get () in
+  match cpp_cmd = "", using_default_cpp, preprocessor_is_gnu_like with
+  | true, true, true -> Gnu
+  | true, true, false -> Not_gnu
+  | _, _, _ -> cpp_opt_kind ()
+
 (* the preprocessor command is:
    If the program has an explicit argument -cpp-command "XX -Y"
    (quotes are required by the shell)
@@ -106,40 +117,27 @@ let cpp_opt_kind () =
    else use the command in [Fc_config.preprocessor].*)
 let get_preprocessor_command () =
   let cmdline = Kernel.CppCommand.get() in
-  if cmdline <> "" then begin
-    (cmdline, cpp_opt_kind ())
-  end else begin
-    let gnu =
-      if Fc_config.using_default_cpp then
-        if Fc_config.preprocessor_is_gnu_like then Gnu else Not_gnu
-      else cpp_opt_kind ()
-    in
-    Fc_config.preprocessor, gnu
-  end
+  if cmdline <> "" then cmdline else Fc_config.preprocessor
 
 let from_filename ?cpp f =
-  let cpp, is_gnu_like =
-    let cmdline = Kernel.CppCommand.get() in
-    if cmdline <> "" then
-      cmdline, cpp_opt_kind ()
-    else
-      let extra_flags =
-        try Kernel.CppExtraArgsPerFile.find f
-        with Not_found -> ""
-      in
-      let jcdb_flags = Json_compilation_database.get_flags f in
-      if extra_flags <> "" && 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, gnu =
-        match cpp with
-        | None -> get_preprocessor_command ()
-        | Some cpp -> cpp, cpp_opt_kind ()
-      in
-      let flags = if extra_flags <> "" then [extra_flags] else jcdb_flags in
-      (if flags = [] then cpp else cpp ^ " " ^ String.concat " " flags), gnu
+  let cpp =
+    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
@@ -158,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_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."
@@ -433,9 +431,18 @@ let replace_in_cpp_cmd cmdl supp_args in_file out_file =
   with Not_found ->
     Format.sprintf "%s %s %s -o %s" cmdl supp_args in_file out_file
 
+(* Note: using Pretty_utils.pp_list without forcing '~pre' and '~suf' to
+   be empty strings can lead to issues when the commands are too long and
+   Format's pretty-printer decides to insert newlines.
+   This concatenation function serves as a reminder to avoid using them.
+*)
+let concat_strs ?(pre="") ?(sep=" ") l =
+  if l = [] then ""
+  else pre ^ (String.concat 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;
@@ -474,10 +481,6 @@ let build_cpp_cmd = function
       then [machdep_macro (Kernel.Machdep.get ())]
       else []
     in
-    let extra_args =
-      if Kernel.FramaCStdLib.get() then add_if_gnu "-nostdinc"
-      else []
-    in
     let define_args = "__FRAMAC__" :: define_args in
     (* Hypothesis: the preprocessor does support the arch-related
        options tested when 'configure' was run. *)
@@ -490,45 +493,44 @@ let build_cpp_cmd = function
     if is_gnu_like = Unknown && not (Kernel.CppCommand.is_set ())
        && unsupported_cpp_arch_args <> [] then
       Kernel.warning ~once:true
-        "your preprocessor is not known to handle option(s) `%a', \
+        "your preprocessor is not known to handle option(s) `%s', \
          considered necessary for machdep `%s'. To ensure compatibility \
          between your preprocessor and the machdep, consider using \
          -cpp-command with the appropriate flags. \
-         Your preprocessor is known to support these flags: %a"
-        (Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
-        unsupported_cpp_arch_args (Kernel.Machdep.get ())
-        (Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
-        Fc_config.preprocessor_supported_arch_options;
-    let extra_args =
-      if Kernel.ReadAnnot.get () then
-        if Kernel.PreprocessAnnot.is_set () then
-          if Kernel.PreprocessAnnot.get () then
-            "-dD" :: extra_args
-          else extra_args
-        else
-          let opt = add_if_gnu "-dD" in
-          opt @ extra_args
-      else extra_args
+         Your preprocessor is known to support these flags: %s"
+        (concat_strs unsupported_cpp_arch_args) (Kernel.Machdep.get ())
+        (concat_strs Fc_config.preprocessor_supported_arch_options);
+    let nostdinc_arg =
+      if Kernel.FramaCStdLib.get() then add_if_gnu "-nostdinc"
+      else []
     in
-    let pp_str = Format.pp_print_string in
+    let output_defines_arg =
+      let open Kernel in
+      match ReadAnnot.get (), PreprocessAnnot.is_set (), PreprocessAnnot.get () with
+      | true, true, true -> ["-dD"] (* keep '#defines' in preprocessed output *)
+      | true, true, false -> []
+      | true, false, _ -> add_if_gnu "-dD"
+      | _, _, _ -> []
+    in
+    let gnu_implicit_args = output_defines_arg @ nostdinc_arg in
     let string_of_supp_args extra includes defines =
-      Format.asprintf "%a%a%a"
-        (Pretty_utils.pp_list ~pre:" -I" ~sep:" -I" ~empty:"" pp_str) includes
-        (Pretty_utils.pp_list ~pre:" -D" ~sep:" -D" ~empty:"" pp_str) defines
-        (Pretty_utils.pp_list ~pre:" " ~sep:" " ~empty:"" pp_str) extra
+      Format.asprintf "%s%s%s"
+        (concat_strs ~pre:"-I" ~sep:" -I" includes)
+        (concat_strs ~pre:" -D" ~sep:" -D" defines)
+        (concat_strs ~pre:" " ~sep:" " extra)
     in
     let supp_args =
       string_of_supp_args
-        (Kernel.CppExtraArgs.get () @ extra_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\""
+      "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,14 +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 %a"
-            (Pretty_utils.pp_list ~sep:" " Format.pp_print_string)
-            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;
@@ -640,7 +637,7 @@ let to_cil_cabs cpp_cmds_and_args f =
 let () =
   let handle f =
     let preprocess =
-      replace_in_cpp_cmd (fst (get_preprocessor_command ())) "-nostdinc"
+      replace_in_cpp_cmd (get_preprocessor_command ()) "-nostdinc"
     in
     let ppf =
       try Logic_preprocess.file ".c" preprocess f
diff --git a/src/kernel_services/ast_queries/file.mli b/src/kernel_services/ast_queries/file.mli
index 0498ef145a6f1abd70ada90149e8b6a92cfd1e54..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
@@ -142,8 +146,10 @@ val get_suffixes: unit -> string list
 val get_name: t -> string
 (** File name (not normalized). *)
 
-val get_preprocessor_command: unit -> string * cpp_opt_kind
-(** Return the preprocessor command to use. *)
+val get_preprocessor_command: unit -> string
+(** Return the preprocessor command to use.
+    @modify Frama-C+dev return type now contains only the command
+*)
 
 val pre_register: t -> unit
 (** Register some file as source file before command-line files *)
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ml b/src/kernel_services/ast_queries/json_compilation_database.ml
index b887b1c358aebafc60096757824855a74850f76e..1c0975165dce9be985b2b299ec8a1e35dd7f77ce 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ml
@@ -131,48 +131,14 @@ let split_command_args s =
     never need quotes. *)
 let quote_define_argument arg = Format.sprintf "%S" arg
 
-let parse_entry jcdb_dir r =
-  let open Yojson.Basic.Util in
-  let filename = r |> member "file" |> to_string in
-  let dirname  = r |> member "directory" |> to_string_option |> Option.value ~default:jcdb_dir in
-  let dirname =
-    if Filename.is_relative dirname then Filename.concat jcdb_dir dirname
-    else dirname
-  in
-  let dirname = Filepath.normalize dirname in
-  let path = Datatype.Filepath.of_string ~base_name:dirname filename in
-
-  (* get the list of arguments, and a flag indicating if the arguments
-     were given via 'command' or 'arguments'; the latter require quoting *)
-  let string_option_list, requote =
-    (* Note: the JSON Compilation Databse specification specifies that
-       "either arguments or command is required", but does NOT specify what
-       happens when both are present. There is a LLVM commit from 2015
-       (https://reviews.llvm.org/D10365) that mentions:
-       "Arguments and Command can now be in the same compilation database for
-        the same file. Arguments are preferred when both are present."
-       The code below follows this behavior. *)
-    try
-      let args = List.map to_string (r |> member "arguments" |> to_list) in
-      args, true
-    with _ ->
-    try
-      let s = r |> member "command" |> to_string in
-      split_command_args s, false
-    with _ ->
-      Kernel.abort "compilation database: expected 'arguments' or 'command'"
-  in
-  (* conversion for '-I' flags *)
-  let convert_path arg =
-    if Filename.is_relative arg then Filename.concat dirname arg
-    else arg
-  in
+(* Filters and normalize useful flags: -I, -D, -U, ... *)
+let filter_useful_flags ~requote option_list =
   let convert_define arg =
     if requote then quote_define_argument arg else arg
   in
   let process_prefix prefix suffix =
     match prefix with
-    | Path s -> s ^ convert_path suffix
+    | Path s -> s ^ suffix
     | Define s -> s ^ convert_define suffix
     | Undefine s -> s ^ suffix
   in
@@ -208,24 +174,30 @@ let parse_entry jcdb_dir r =
             let new_arg = process_prefix prefix arg in
             (None, new_arg :: acc_res)
           end
-      ) (None, []) string_option_list
+      ) (None, []) option_list
   in
-  (* 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 replace them with the latest ones found, warning the
-     user if previous flags were different. *)
-  let flags = List.rev res in
+  List.rev res
+
+(* 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 replace them with the latest ones found, warning the
+   user if previous flags were different. *)
+let update_flags_verbosely path flags =
   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_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_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"
@@ -239,6 +211,40 @@ let parse_entry jcdb_dir r =
   | Not_found ->
     Flags.add path flags
 
+let parse_compilation_entry jcdb_dir r =
+  let open Yojson.Basic.Util in
+  let filename = r |> member "file" |> to_string in
+  let dirname  = r |> member "directory" |> to_string_option |> Option.value ~default:jcdb_dir in
+  let dirname =
+    if Filename.is_relative dirname then Filename.concat jcdb_dir dirname
+    else dirname
+  in
+  let dirname = Filepath.normalize dirname in
+  let path = Datatype.Filepath.of_string ~base_name:dirname filename in
+
+  (* get the list of arguments, and a flag indicating if the arguments
+     were given via 'command' or 'arguments'; the latter require quoting *)
+  let string_option_list, requote =
+    (* Note: the JSON Compilation Database specification specifies that
+       "either arguments or command is required", but does NOT specify what
+       happens when both are present. There is a LLVM commit from 2015
+       (https://reviews.llvm.org/D10365) that mentions:
+       "Arguments and Command can now be in the same compilation database for
+        the same file. Arguments are preferred when both are present."
+       The code below follows this behavior. *)
+    try
+      let args = List.map to_string (r |> member "arguments" |> to_list) in
+      args, true
+    with _ ->
+    try
+      let s = r |> member "command" |> to_string in
+      split_command_args s, false
+    with _ ->
+      Kernel.abort "compilation database: expected 'arguments' or 'command'"
+  in
+  let flags = filter_useful_flags ~requote string_option_list in
+  update_flags_verbosely path flags
+
 let compute_flags_from_file () =
   let database = (Kernel.JsonCompilationDatabase.get () :> string) in
   let jcdb_dir, jcdb_path =
@@ -253,7 +259,7 @@ let compute_flags_from_file () =
       let r_list =
         Yojson.Basic.from_file jcdb_path |> Yojson.Basic.Util.to_list
       in
-      List.iter (parse_entry jcdb_dir) r_list;
+      List.iter (parse_compilation_entry jcdb_dir) r_list;
     with
     | Sys_error msg
     | Yojson.Json_error msg
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 5c30b36f614a0626ebb02eadf0d57c285e1bc164..d75e4af4d4fcd3cf61efe2ce32ce5f55fe2aeb12 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -86,6 +86,7 @@ let dkey_rmtmps = register_category "parser:rmtmps"
 let dkey_referenced = register_category "parser:referenced"
 
 let dkey_pp = register_category "pp"
+let dkey_pp_logic = register_category "pp:logic"
 let dkey_compilation_db = register_category "pp:compilation-db"
 
 let dkey_print_bitfields = register_category "printer:bitfields"
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 7bc32e34f8dab6d63026eb7f62aa7b3f4c49bf72..172ab5ef8db94074398185d234316ea7d78fb129 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -83,6 +83,8 @@ val dkey_parser: category
 
 val dkey_pp: category
 
+val dkey_pp_logic: category
+
 val dkey_print_attrs: category
 
 val dkey_print_bitfields: category
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..5dfc21439f01527a4f67a7a1ebcb44a153b668b7
--- /dev/null
+++ b/tests/jcdb/logic-pp-include/no-stdio.c
@@ -0,0 +1,7 @@
+// compile_commands.json must have "-includestdio.h" and define ZERO
+
+//@ ensures \result == 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..a8432079471806a65084e802c433a6492980d71e
--- /dev/null
+++ b/tests/jcdb/oracle/logic-pp-include.res
@@ -0,0 +1,16 @@
+[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"
+/*@ ensures \result ≡ 0; */
+int main(void)
+{
+  int __retres;
+  printf("bla\n");
+  __retres = 0;
+  return __retres;
+}
+
+
diff --git a/tests/syntax/cpp-command.c b/tests/syntax/cpp-command.c
index b508b543b6b25745f437b481935ab3e1add8fa02..4a533887e76e6e5ee719c0efaec0174c0414c3bb 100644
--- a/tests/syntax/cpp-command.c
+++ b/tests/syntax/cpp-command.c
@@ -1,8 +1,18 @@
 /* run.config*
-   FILTER: sed "s:/[^ ]*/cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::; s: -m32::"
+   FILTER: sed "s:/[^ ]*[/]cpp-command\.[^ ]*\.i:TMPDIR/FILE.i:g; s:$PWD/::; s: -m32::"
    OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']"
    OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'"
    OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\""
    OPT: -machdep x86_32 -no-autoload-plugins -cpp-frama-c-compliant -cpp-command "echo %var is not an interpreted placeholder"
    OPT: -machdep x86_32 -no-autoload-plugins -print-cpp-commands
+   OPT: -cpp-extra-args-per-file=@PTEST_FILE@:"-DPF=\\\"cp%02d_3f\\\"" -no-autoload-plugins @PTEST_FILE@ -print
    */
+
+#include <stdio.h>
+void printer(int i, float f) {
+  printf(PF, i, f);
+}
+
+int main() {
+  printer(1, 1.0);
+}
diff --git a/tests/syntax/oracle/cpp-command.0.res.oracle b/tests/syntax/oracle/cpp-command.0.res.oracle
index 52bfebffa2b2199998d087475431714d90ccffb9..f910fe5ece81818d84c0dab9a4af138213c8ffa8 100644
--- a/tests/syntax/oracle/cpp-command.0.res.oracle
+++ b/tests/syntax/oracle/cpp-command.0.res.oracle
@@ -1,2 +1,2 @@
 [kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
-[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] [ -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc]
+[cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i TMPDIR/FILE.i] [-I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc]
diff --git a/tests/syntax/oracle/cpp-command.1.res.oracle b/tests/syntax/oracle/cpp-command.1.res.oracle
index 9fa845eca34510435741d8e8e4303e5969fb7434..4d07269a88da2aca64a17efaba30377dfd8fcaab 100644
--- a/tests/syntax/oracle/cpp-command.1.res.oracle
+++ b/tests/syntax/oracle/cpp-command.1.res.oracle
@@ -1,2 +1,2 @@
 [kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
-%1 = cpp-command.c %2 = TMPDIR/FILE.i %args =  -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc
+%1 = cpp-command.c %2 = TMPDIR/FILE.i %args = -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc
diff --git a/tests/syntax/oracle/cpp-command.4.res.oracle b/tests/syntax/oracle/cpp-command.4.res.oracle
index 2008e719f9d6ebf04f9f1ef71946c37a79d60f88..2f8d187fc5edca6bf9ef78bff98609317dc67759 100644
--- a/tests/syntax/oracle/cpp-command.4.res.oracle
+++ b/tests/syntax/oracle/cpp-command.4.res.oracle
@@ -1,2 +1,2 @@
 [kernel] Preprocessing command:
-  gcc -E -C -I.  -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc 'tests/syntax/cpp-command.c' -o 'TMPDIR/FILE.i'
+  gcc -E -C -I. -I./share/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc 'tests/syntax/cpp-command.c' -o 'TMPDIR/FILE.i'
diff --git a/tests/syntax/oracle/cpp-command.5.res.oracle b/tests/syntax/oracle/cpp-command.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..72e8b677b25bad905a4dda20d59cb6f552481de4
--- /dev/null
+++ b/tests/syntax/oracle/cpp-command.5.res.oracle
@@ -0,0 +1,21 @@
+[kernel] Parsing tests/syntax/cpp-command.c (with preprocessing)
+/* Generated by Frama-C */
+#include "errno.h"
+#include "stdarg.h"
+#include "stddef.h"
+#include "stdio.h"
+void printer(int i, float f)
+{
+  printf("cp%02d_3f",i,(double)f);
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  printer(1,(float)1.0);
+  __retres = 0;
+  return __retres;
+}
+
+