diff --git a/Makefile.generating b/Makefile.generating
index b98dc5e96ebec884e0559f3d21522b5b5d53c8f9..5aeabb3e2bab9cf4e171db282b4f97205c5ad26e 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -31,13 +31,13 @@ tests/ptests_config: Makefile.generating share/Makefile.config
$(RM) $@
$(TOUCH) $@
$(ECHO) "DEFAULT_SUITES=$(PLUGIN_TESTS_LIST)" >> $@
- $(ECHO) "TOPLEVEL_PATH=bin/toplevel.$(OCAMLBEST)$(EXE)" >> $@
+ $(ECHO) "TOPLEVEL_PATH=$(FRAMAC_ROOT_SRCDIR)/bin/toplevel.$(OCAMLBEST)$(EXE)" >> $@
$(ECHO) "OCAMLRUNPARAM=" >> $@
- $(ECHO) "FRAMAC_SESSION=." >> $@
- $(ECHO) "FRAMAC_SHARE=./share" >> $@
- $(ECHO) "FRAMAC_PLUGIN=./lib/plugins" >> $@
- $(ECHO) "FRAMAC_PLUGIN_GUI=./lib/plugins/gui" >> $@
- $(ECHO) "FRAMAC_LIB=./lib/fc" >> $@
+ $(ECHO) "FRAMAC_SESSION=$(FRAMAC_ROOT_SRCDIR)" >> $@
+ $(ECHO) "FRAMAC_SHARE=$(FRAMAC_ROOT_SRCDIR)/share" >> $@
+ $(ECHO) "FRAMAC_PLUGIN=$(FRAMAC_ROOT_SRCDIR)/lib/plugins" >> $@
+ $(ECHO) "FRAMAC_PLUGIN_GUI=$(FRAMAC_ROOT_SRCDIR)/lib/plugins/gui" >> $@
+ $(ECHO) "FRAMAC_LIB=$(FRAMAC_ROOT_SRCDIR)/lib/fc" >> $@
$(CHMOD_RO) $@
ALL_LIBRARY_NAMES=$(shell ocamlfind query -r -p-format $(LIBRARY_NAMES) $(LIBRARY_NAMES_GUI))
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index cdfbd925143a3e48433def70169c98517dcb2380..5d1fcf6df5ba8b1b970c07a1839698788108074b 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -523,10 +523,23 @@ let build_cpp_cmd = function
include_args define_args
in
let cpp_command = replace_in_cpp_cmd cmdl supp_args (f:>string) (ppf:>string) in
+ let cpp_command_with_chdir =
+ if Kernel.JsonCompilationDatabase.is_set () then
+ let jcdb_path = (Kernel.JsonCompilationDatabase.get () :> string) in
+ let dir =
+ if Sys.is_directory jcdb_path then jcdb_path
+ else Filename.dirname jcdb_path
+ in
+ let cwd = Unix.getcwd () in
+ if cwd <> dir then
+ "cd " ^ dir ^ " && " ^ cpp_command
+ else cpp_command
+ else cpp_command
+ in
Kernel.feedback ~dkey:Kernel.dkey_pp
"preprocessing with \"%s\""
- cpp_command;
- Some (cpp_command, ppf, supp_args)
+ cpp_command_with_chdir;
+ Some (cpp_command_with_chdir, ppf, supp_args)
let parse_cabs cpp_command = function
| NoCPP f ->
@@ -1744,17 +1757,17 @@ let prepare_from_c_files () =
let files = Files.get () in (* Allow pre-registration of prolog files *)
let cpp_commands = List.map (fun f -> (f, build_cpp_cmd f)) files in
if Kernel.PrintCppCommands.get () then print_and_exit cpp_commands;
- if not (Kernel.AuditCheck.is_empty ()) then begin
+ let audit_check_path = Kernel.AuditCheck.get () in
+ if not (Filepath.Normalized.is_empty audit_check_path) then begin
let all_sources_tbl = compute_sources_table cpp_commands in
- let expected_hashes = source_hashes_of_json (Kernel.AuditCheck.get ()) in
+ let expected_hashes = source_hashes_of_json audit_check_path in
check_source_hashes expected_hashes all_sources_tbl
end;
- if not (Kernel.AuditPrepare.is_empty ()) then begin
+ let audit_path = Kernel.AuditPrepare.get () in
+ if not (Filepath.Normalized.is_empty audit_path) then begin
let all_sources_tbl = compute_sources_table cpp_commands in
- let audit_path = Kernel.AuditPrepare.get () in
print_all_sources audit_path all_sources_tbl;
- if not (Filepath.Normalized.is_special_stdout audit_path)
- then
+ if not (Filepath.Normalized.is_special_stdout audit_path) then
Kernel.feedback "Audit: sources list written to: %a@."
Filepath.Normalized.pretty audit_path;
end;
diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml
index 4fb1fe39b1174c208bfbe293d73e1b50c95b1dad..aee2fb64e6cba33139387c964db365fd8df2bdd5 100644
--- a/src/kernel_services/cmdline_parameters/cmdline.ml
+++ b/src/kernel_services/cmdline_parameters/cmdline.ml
@@ -268,10 +268,10 @@ exception Cannot_parse of string * string
let raise_error name because = raise (Cannot_parse(name, because))
let error name msg =
- let bin_name = Sys.argv.(0) in
+ let bin_name = Filepath.Normalized.of_string Sys.argv.(0) in
Kernel_log.abort
- "option `%s' %s.@\nuse `%s -help' for more information."
- name msg bin_name
+ "option `%s' %s.@\nuse `%a -help' for more information."
+ name msg Filepath.Normalized.pretty bin_name
let warning name msg =
Kernel_log.warning
diff --git a/tests/jcdb/compile_commands.json b/tests/jcdb/compile_commands.json
index 0592cf2b0799160bb9d83ce1b7aa103c2fc15b7c..0636253c51623f06ae390c688eb0c77254aad822 100644
--- a/tests/jcdb/compile_commands.json
+++ b/tests/jcdb/compile_commands.json
@@ -1,10 +1,10 @@
[
{ "directory": ".",
- "command": "g++ -DDUPLICATE_FLAGS_THAT_WILL_BE_OVERWRITTEN",
+ "command": "gcc -DDUPLICATE_FLAGS_THAT_WILL_BE_OVERWRITTEN",
"file": "jcdb.c"
},
{ "directory": ".",
- "command": "g++ -DDUPLICATE_FLAGS_THAT_WILL_BE_OVERWRITTEN",
+ "command": "gcc -DDUPLICATE_FLAGS_THAT_WILL_BE_OVERWRITTEN",
"file": "jcdb.c"
},
{
@@ -12,7 +12,7 @@
"file": "jcdb.c"
},
{ "directory": ".",
- "command": "/usr/bin/clang++ -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",
+ "command": "/usr/bin/clang -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",
"file": "jcdb.c"
}
]
diff --git a/tests/jcdb/oracle/subdir.err b/tests/jcdb/oracle/subdir.err
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/jcdb/oracle/subdir.res b/tests/jcdb/oracle/subdir.res
new file mode 100644
index 0000000000000000000000000000000000000000..db55f314d60304947e9a79782ccf41d22e986345
--- /dev/null
+++ b/tests/jcdb/oracle/subdir.res
@@ -0,0 +1 @@
+[kernel] Parsing PWD/../subdir.c (with preprocessing)
diff --git a/tests/jcdb/subdir.c b/tests/jcdb/subdir.c
new file mode 100644
index 0000000000000000000000000000000000000000..1729358186a7ea3555027ab353b3194e7a8692e5
--- /dev/null
+++ b/tests/jcdb/subdir.c
@@ -0,0 +1,13 @@
+/* run.config
+ NOFRAMAC:
+ EXECNOW: LOG subdir.res LOG subdir.err (cd @PTEST_DIR@/subdir1 && @frama-c@ -add-symbolic-path $PWD/..:PWD/.. -json-compilation-database ../subdir.json ../subdir.c) > @PTEST_RESULT@/subdir.res 2> @PTEST_RESULT@/subdir.err
+*/
+
+// this test must be run with PWD in subdir1
+#include "subdir1/header.h"
+#include "included.h" // in subdir2, via '-Isubdir2' in subdir.json
+#include "__fc_builtin.h" // to check that Frama-C's libc is correctly included
+
+int main() {
+ return ONE + TWO;
+}
diff --git a/tests/jcdb/subdir.json b/tests/jcdb/subdir.json
new file mode 100644
index 0000000000000000000000000000000000000000..05879db42ad96969ed354f37842b5dfb617b3685
--- /dev/null
+++ b/tests/jcdb/subdir.json
@@ -0,0 +1,6 @@
+[
+ { "directory": ".",
+ "command": "gcc -Isubdir2",
+ "file": "subdir.c"
+ }
+]
diff --git a/tests/jcdb/subdir1/header.h b/tests/jcdb/subdir1/header.h
new file mode 100644
index 0000000000000000000000000000000000000000..f01809a81bd36dc763f39331fbce25d55b2d5651
--- /dev/null
+++ b/tests/jcdb/subdir1/header.h
@@ -0,0 +1 @@
+#define ONE 1
diff --git a/tests/jcdb/subdir2/included.h b/tests/jcdb/subdir2/included.h
new file mode 100644
index 0000000000000000000000000000000000000000..80ba189555ec881b79013d40798117477b1086d0
--- /dev/null
+++ b/tests/jcdb/subdir2/included.h
@@ -0,0 +1,3 @@
+// to be included by subdir.c
+
+#define TWO 2