diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index c71b094486f17fc7bbd2bb146716097f51c9583e..8378c48b20a8d8a50015aae135dca2a72b1fddca 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -530,7 +530,13 @@ let build_cpp_cmd = function
if Sys.is_directory jcdb_path then jcdb_path
else Filename.dirname jcdb_path
in
- let cwd = Unix.getcwd () in
+ (* TODO: we currently use PWD instead of Sys.getcwd () because OCaml has
+ no function in its stdlib to resolve symbolic links (e.g. realpath)
+ for a given path. 'getcwd' always resolves them, but if the user
+ supplies a path with symbolic links, this may cause issues.
+ Instead of forcing the user to always provide resolved paths, we
+ currently choose to never resolve them. *)
+ let cwd = Unix.getenv "PWD" in
if cwd <> dir then
"cd " ^ dir ^ " && " ^ cpp_command
else cpp_command
diff --git a/src/kernel_services/plugin_entry_points/journal.ml b/src/kernel_services/plugin_entry_points/journal.ml
index 630371b8ee7d0268a69d79bbe876263e99ffa37a..b08df75e43675d0634a68323ef0e7c36cb45360e 100644
--- a/src/kernel_services/plugin_entry_points/journal.ml
+++ b/src/kernel_services/plugin_entry_points/journal.ml
@@ -142,7 +142,7 @@ let print_trailer fmt =
Format.fprintf fmt "@[(* Main *)@]@\n";
Format.fprintf fmt "@[<hv 2>let main () =@;";
Format.fprintf fmt
- "@[<hv 0>@[<hv 2>Journal.keep_file@;\"%s\";@]@;"
+ "@[<hv 0>@[<hv 2>Journal.keep_file@; (Datatype.Filepath.of_string@; (\"%s\"));@]@;"
name;
Format.fprintf fmt "try run ()@;";
Format.fprintf fmt "@[<v>with@;@[<hv 2>| Unreachable ->@ ";
@@ -170,14 +170,15 @@ let print_trailer fmt =
(* close the outermost box *)
Format.pp_close_box fmt ()
-let preserved_files = ref []
+let preserved_files : Datatype.Filepath.t list ref = ref []
let keep_file s = preserved_files := s :: !preserved_files
let get_filename =
let cpt = ref 0 in
let rec get_filename first =
- let name = Format.asprintf "%a" Datatype.Filepath.pretty (get_name ()) in
- if (not first && Sys.file_exists name) || List.mem name !preserved_files
+ let name_fp = get_name () in
+ let name = (name_fp:>string) in
+ if (not first && Sys.file_exists name) || List.mem name_fp !preserved_files
then begin
incr cpt;
let suf = "_" ^ string_of_int !cpt in
@@ -193,7 +194,7 @@ let get_filename =
filename := name ^ suf);
get_filename false
end else
- name
+ name_fp
in
fun () -> get_filename true
@@ -208,9 +209,10 @@ let write () =
in
let error msg s = error "cannot %s journal (%s)." msg s in
let filename = get_filename () in
- feedback "writing journal in file `%s'." filename;
+ feedback "writing journal in file `%a'."
+ Datatype.Filepath.pretty filename;
try
- let cout = open_out filename in
+ let cout = open_out (filename:>string) in
let fmt = Format.formatter_of_out_channel cout in
Format.pp_set_margin fmt 78 (* line length *);
(try write fmt with Sys_error s -> error "write into" s);
diff --git a/src/kernel_services/plugin_entry_points/journal.mli b/src/kernel_services/plugin_entry_points/journal.mli
index b3e63d7548ed5b293b0a28f1634136c94147504d..01fcade163a4999bd2a65c5b102022dfe1726fc0 100644
--- a/src/kernel_services/plugin_entry_points/journal.mli
+++ b/src/kernel_services/plugin_entry_points/journal.mli
@@ -106,8 +106,8 @@ val restore: unit -> unit
(** {2 Internal use only} *)
(* ****************************************************************************)
-val keep_file: string -> unit
-(** This function has not to be used explicitly. Only offers functions
+val keep_file: Datatype.Filepath.t -> unit
+(** This function is not to be used explicitly. Only offers functions
retrieving when running a journal file. *)
val get_session_file: (string -> Datatype.Filepath.t) ref
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 81dd5d8eff799578387253afebeff39a9592a2f7..6f1a5cb5e270e4a40a183ed8c013e4607534e3de 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -125,7 +125,13 @@ let insert base path_name =
Array.set cache (hash land 255) (Some (path_name, path));
path
-let cwd = insert dummy (Sys.getcwd())
+(* TODO: we currently use PWD instead of Sys.getcwd () because OCaml has
+ no function in its stdlib to resolve symbolic links (e.g. realpath)
+ for a given path. 'getcwd' always resolves them, but if the user
+ supplies a path with symbolic links, this may cause issues.
+ Instead of forcing the user to always provide resolved paths, we
+ currently choose to never resolve them. *)
+let cwd = insert dummy (Sys.getenv "PWD")
type existence =
| Must_exist
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index fc33b7542ff6d3b3d37335fed4c740d0ee1afc02..52d493fe3f97bbc0da6dc96fa8348af2fc778771 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -255,7 +255,14 @@ let gen_run remarks =
(key, (dir :> string))
) (Filepath.all_symbolic_dirs ())
in
- let uriBases = ("PWD", Sys.getcwd ()) :: symbolicDirs in
+ (* TODO: we currently use Sys.getenv "PWD" instead of Sys.getcwd ()
+ because OCaml has no function in its stdlib to resolve symbolic links
+ (e.g. realpath) for a given path.
+ 'getcwd' always resolves them, but if the user supplies a path with
+ symbolic links, this may cause issues.
+ Instead of forcing the user to always provide resolved paths, we
+ currently choose to never resolve them. *)
+ let uriBases = ("PWD", Sys.getenv "PWD") :: symbolicDirs in
let uriBasesJson =
List.fold_left (fun acc (name, dir) ->
let baseUri =
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 955cb0988ace3a74cf08f6add2c16d7b22aa778b..bc8d07ce81572eac4495c12ea67cfd3d7870dae9 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1206,7 +1206,13 @@ let get_output_dir d =
(* --- Session dir --- *)
(* -------------------------------------------------------------------------- *)
-let default = Sys.getcwd () ^ "/.frama-c"
+(* TODO: we currently use PWD instead of Sys.getcwd () because OCaml has
+ no function in its stdlib to resolve symbolic links (e.g. realpath)
+ for a given path. 'getcwd' always resolves them, but if the user
+ supplies a path with symbolic links, this may cause issues.
+ Instead of forcing the user to always provide resolved paths, we
+ currently choose to never resolve them. *)
+let default = Sys.getenv "PWD" ^ "/.frama-c"
let has_session () =
Session.is_set () ||