diff --git a/share/analysis-scripts/list_functions.ml b/share/analysis-scripts/list_functions.ml
index 4bf75dc70a1bb9763f12f18e9c7c03d695cebd2d..6d9ccb92d3ac2b520fddec81c834251b58d2c83a 100644
--- a/share/analysis-scripts/list_functions.ml
+++ b/share/analysis-scripts/list_functions.ml
@@ -115,8 +115,7 @@ class stmt_count_visitor =
location-based approach. *)
let located_within_framac_libc loc =
let pos = fst loc in
- let file = (pos.Filepath.pos_path :> string) in
- Filepath.is_relative ~base_name:Fc_config.framac_libc file
+ Filepath.is_relative ~base_name:Fc_config.framac_libc pos.Filepath.pos_path
class fun_cabs_visitor print_libc = object(self)
inherit Cabsvisit.nopCabsVisitor
diff --git a/src/kernel_internals/runtime/dump_config.ml b/src/kernel_internals/runtime/dump_config.ml
index 432a53c8517f660f045174ddc2f046b58c73ca6e..5774f5bba245230d110686c4bc2c985e4e1ab463 100644
--- a/src/kernel_internals/runtime/dump_config.ml
+++ b/src/kernel_internals/runtime/dump_config.ml
@@ -55,11 +55,13 @@ let dump_to_json () =
"ocamlc", `String Fc_config.ocamlc ;
"ocamlopt", `String Fc_config.ocamlopt ;
"ocaml_wflags", `String Fc_config.ocaml_wflags ;
- "datadir", `String Fc_config.datadir ;
- "datadirs", list string Fc_config.datadirs ;
+ "datadir", `String (Fc_config.datadir:>string) ;
+ "datadirs",
+ list string (Filepath.Normalized.to_string_list Fc_config.datadirs) ;
"framac_libc", `String (Fc_config.framac_libc:>string) ;
- "libdir", `String Fc_config.libdir ;
- "plugin_dir", list string Fc_config.plugin_dir ;
+ "libdir", `String (Fc_config.libdir:>string) ;
+ "plugin_dir",
+ list string (Filepath.Normalized.to_string_list Fc_config.plugin_dir) ;
"plugin_path", `String Fc_config.plugin_path ;
"compilation_unit_names", list string Fc_config.compilation_unit_names ;
"library_names", list string Fc_config.library_names ;
diff --git a/src/kernel_internals/runtime/fc_config.ml.in b/src/kernel_internals/runtime/fc_config.ml.in
index b7980cdeba96e77af39ef763d274546e3a3c148f..7e76be13a3488fcf4af8730e3b22f4b9cd74118a 100644
--- a/src/kernel_internals/runtime/fc_config.ml.in
+++ b/src/kernel_internals/runtime/fc_config.ml.in
@@ -38,9 +38,10 @@ let ocamlc = "@OCAMLC@"
let ocamlopt = "@OCAMLOPT@"
let ocaml_wflags = "@WARNINGS@"
-let getenv_list name =
+let getenv_list name : Filepath.Normalized.t list =
let path = Sys.getenv name in
- Str.split (Str.regexp ":") path
+ let dirs = Str.split (Str.regexp ":") path in
+ List.map Filepath.Normalized.of_string dirs
let add_symbolic_dir_list name = function
| [d] -> Filepath.add_symbolic_dir name d
@@ -52,8 +53,10 @@ let add_symbolic_dir_list name = function
ds
-let datadir = try Sys.getenv "FRAMAC_SHARE" with Not_found -> "@FRAMAC_DATADIR@"
-let framac_libc = Filepath.Normalized.of_string (datadir ^ "/libc")
+let datadir =
+ Filepath.Normalized.of_string
+ (try Sys.getenv "FRAMAC_SHARE" with Not_found -> "@FRAMAC_DATADIR@")
+let framac_libc = Filepath.Normalized.concat datadir "libc"
let extra_datadir = try getenv_list "FRAMAC_EXTRA_SHARE" with Not_found -> []
let () = add_symbolic_dir_list "FRAMAC_EXTRA_SHARE" extra_datadir
(** After so that it has the priority for pretty printing *)
@@ -61,16 +64,24 @@ let () = Filepath.add_symbolic_dir "FRAMAC_SHARE" datadir
let datadirs = datadir::extra_datadir
-let libdir = try Sys.getenv "FRAMAC_LIB" with Not_found -> "@FRAMAC_LIBDIR@"
+let libdir =
+ Filepath.Normalized.of_string
+ (try Sys.getenv "FRAMAC_LIB" with Not_found -> "@FRAMAC_LIBDIR@")
let () = Filepath.add_symbolic_dir "FRAMAC_LIB" libdir
let plugin_dir =
try
getenv_list "FRAMAC_PLUGIN"
with Not_found ->
- try [ Sys.getenv "FRAMAC_LIB" ^ "/plugins" ]
- with Not_found -> [ "@FRAMAC_PLUGINDIR@" ]
-
-let plugin_path = String.concat ":" plugin_dir
+ try
+ let dir =
+ Filepath.Normalized.concat
+ (Filepath.Normalized.of_string (Sys.getenv "FRAMAC_LIB")) "plugins"
+ in
+ [dir]
+ with Not_found -> [ Filepath.Normalized.of_string "@FRAMAC_PLUGINDIR@" ]
+
+let plugin_path =
+ String.concat ":" (Filepath.Normalized.to_string_list plugin_dir)
let () = add_symbolic_dir_list "FRAMAC_PLUGIN" plugin_dir
diff --git a/src/kernel_internals/runtime/fc_config.mli b/src/kernel_internals/runtime/fc_config.mli
index 26c5c4484d823b3b065bf9f883692c22a294c17d..47ba665d964429c5a95e0782c7657cc2ff4f469f 100644
--- a/src/kernel_internals/runtime/fc_config.mli
+++ b/src/kernel_internals/runtime/fc_config.mli
@@ -62,11 +62,11 @@ val ocaml_wflags: string
(** Warning flags used when compiling Frama-C.
@since Chlorine-20180501 *)
-val datadir: string
+val datadir: Filepath.Normalized.t
(** Directory where architecture independent files are.
Main directory, use {!datadirs} for the others *)
-val datadirs: string list
+val datadirs: Filepath.Normalized.t list
(** Directories where architecture independent files are in order of
priority.
@since 19.0-Potassium *)
@@ -75,16 +75,16 @@ val framac_libc: Filepath.Normalized.t
(** Directory where Frama-C libc headers are.
@since 19.0-Potassium *)
-val libdir: string
+val libdir: Filepath.Normalized.t
(** Directory where the Frama-C kernel library is.
@since Beryllium-20090601-beta1 *)
-val plugin_dir: string list
+val plugin_dir: Filepath.Normalized.t list
(** Directory where the Frama-C dynamic plug-ins are.
@modify Magnesium-20151001 *)
val plugin_path: string
-(** The coma-separated concatenation of [plugin_dir].
+(** The colon-separated concatenation of [plugin_dir].
@since Magnesium-20151001 *)
val compilation_unit_names: string list
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index e0edf8abfab073a2744df8bb1db580eae191c358..740ac2767d634aacad3861ebe462f01fda248b0c 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -34,7 +34,8 @@ let print_config () =
FRAMAC_LIB = %S@\n \
FRAMAC_PLUGIN = %S%t@."
Fc_config.version_and_codename
- Fc_config.datadir Fc_config.libdir Fc_config.plugin_path
+ (Fc_config.datadir:>string) (Fc_config.libdir:>string)
+ Fc_config.plugin_path
(fun fmt ->
if Fc_config.preprocessor = "" then
Format.fprintf fmt "@\nWarning: no default pre-processor"
@@ -58,10 +59,12 @@ let print_version =
print_config Kernel.PrintVersion.get Fc_config.version_and_codename
let () = Cmdline.run_after_early_stage print_version
-let print_sharepath = print_config Kernel.PrintShare.get Fc_config.datadir
+let print_sharepath =
+ print_config Kernel.PrintShare.get (Fc_config.datadir:>string)
let () = Cmdline.run_after_early_stage print_sharepath
-let print_libpath = print_config Kernel.PrintLib.get Fc_config.libdir
+let print_libpath =
+ print_config Kernel.PrintLib.get (Fc_config.libdir:>string)
let () = Cmdline.run_after_early_stage print_libpath
let print_pluginpath =
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 4f0f261cc0df7de4731f2b911a22d0b3c5cc7677..14a582606bae3a9f1b973bb551b4b22a61ece9fd 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -246,7 +246,7 @@ let load_script base =
else
Format.fprintf fmt "%s -c" Fc_config.ocamlc ;
Format.fprintf fmt
- " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags Fc_config.libdir ;
+ " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags (Fc_config.libdir :> string) ;
if !Fc_config.is_gui && Fc_config.lablgtk <> "" then
Format.fprintf fmt " -package %s" Fc_config.lablgtk;
List.iter (fun p -> Format.fprintf fmt " -I %s" p) !load_path ;
@@ -285,11 +285,13 @@ let set_module_load_path path =
if is_dir d then d::ps else
( if user then Klog.warning "cannot load '%s' (not a directory)" d
; ps ) in
+ let plugin_path = Filepath.Normalized.to_string_list Fc_config.plugin_dir in
Klog.debug ~dkey "plugin_dir: %s"
- (String.concat ocamlfind_path_separator Fc_config.plugin_dir);
+ (String.concat ocamlfind_path_separator plugin_path);
load_path :=
List.fold_right (add_dir ~user:true) path
- (List.fold_right (add_dir ~user:false) (Fc_config.libdir::Fc_config.plugin_dir) []);
+ (List.fold_right (add_dir ~user:false)
+ ((Fc_config.libdir :> string) :: plugin_path) []);
let env_ocamlpath =
try Str.split (Str.regexp ocamlfind_path_separator) (Sys.getenv "OCAMLPATH")
with Not_found -> []
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 8b30799b24b82fa49b74dde6e385e750b5dc3191..41d619a4036cff2c18448f4a1f2e3f0c052118c9 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -622,8 +622,7 @@ let () =
(* keep module [Filepath] synchronized with [SymbolicPath] *)
Filepath.reset_symbolic_dirs ();
Datatype.Filepath.Map.iter
- (fun n p -> Filepath.add_symbolic_dir p (n :> string))
- map)
+ (fun n p -> Filepath.add_symbolic_dir p n) map)
(* [SymbolicPath] is better to be not projectified,
but must be saved: use a fake state for saving it without projectifying it *)
@@ -911,10 +910,12 @@ let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.do_not_projectify ()
module Session_dir =
- P.Empty_string
+ P.Filepath
(struct
let option_name = "-session"
- let arg_name = ""
+ let arg_name = "path"
+ let existence = Filepath.Indifferent
+ let file_kind = "directory"
let help = "directory in which session files are searched"
end)
let () = Plugin.session_is_set_ref := Session_dir.is_set
@@ -924,10 +925,12 @@ let () = Parameter_customize.set_cmdline_stage Cmdline.Extending
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.do_not_projectify ()
module Config_dir =
- P.Empty_string
+ P.Filepath
(struct
let option_name = "-config"
- let arg_name = ""
+ let arg_name = "path"
+ let existence = Filepath.Indifferent
+ let file_kind = "directory"
let help = "directory in which configuration files are searched"
end)
let () = Plugin.config_is_set_ref := Config_dir.is_set
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index c971c83111ff2b386bab8668ef9e98ac605a40e2..27b353b4565b05eeea3464f8220183f50528fe9c 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -356,13 +356,17 @@ module Journal: sig
end
-module Session_dir: Parameter_sig.String
+module Session_dir: Parameter_sig.Filepath
(** Directory in which session files are searched.
- @since Neon-20140301 *)
+ @since Neon-20140301
+ @modify Frama-C+dev parameter type is now Filepath instead of string
+*)
-module Config_dir: Parameter_sig.String
+module Config_dir: Parameter_sig.Filepath
(** Directory in which config files are searched.
- @since Neon-20140301 *)
+ @since Neon-20140301
+ @modify Frama-C+dev parameter type is now Filepath instead of string
+*)
(* this stop special comment does not work as expected (and as explained in the
OCamldoc manual, Section 15.2.2. It just skips all the rest of the file
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index caa286cf6bb75d83289d41748c72a141edbd1044..9d7cc4b9cd684bf4e95d79ebc72df86ac8fa64cc 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -300,7 +300,7 @@ struct
module Make_specific_dir
(O: Parameter_sig.Input_with_arg)
(D: sig
- val dirs: unit -> string list
+ val dirs: unit -> Fc_Filepath.Normalized.t list
val visible_ref: bool
end)
=
@@ -351,11 +351,10 @@ struct
let dirs = D.dirs () in
assert (dirs <> []);
if is_kernel
- then
- List.map Datatype.Filepath.of_string dirs
+ then dirs
else
List.map
- (fun x -> Datatype.Filepath.of_string (x ^ "/" ^ plugin_subpath))
+ (fun x -> Datatype.Filepath.concat x plugin_subpath)
dirs
end
@@ -456,8 +455,10 @@ struct
let dirs () = [
if !session_is_set_ref () then !session_ref ()
else
- try Sys.getenv "FRAMAC_SESSION"
- with Not_found -> "./.frama-c"]
+ Fc_Filepath.Normalized.of_string
+ (try Sys.getenv "FRAMAC_SESSION"
+ with Not_found -> "./.frama-c")
+ ]
let visible_ref = !session_visible_ref
end)
let () =
@@ -476,20 +477,24 @@ struct
end)
(struct
let dirs () = [
+ let to_path = Fc_Filepath.Normalized.of_string in
let d, vis =
if !config_is_set_ref () then !config_ref (), false
else
- try Sys.getenv "FRAMAC_CONFIG", false
+ try to_path (Sys.getenv "FRAMAC_CONFIG"), false
with Not_found ->
- try Sys.getenv "USERPROFILE", false (* Win32 *)
+ try to_path (Sys.getenv "USERPROFILE"), false (* Win32 *)
with Not_found ->
(* Unix like *)
- try Sys.getenv "XDG_CONFIG_HOME", true
+ try to_path (Sys.getenv "XDG_CONFIG_HOME"), true
with Not_found ->
- try Sys.getenv "HOME" ^ "/.config", true
- with Not_found -> ".", false
+ try
+ Fc_Filepath.Normalized.concat
+ (to_path (Sys.getenv "HOME")) ".config", true
+ with Not_found -> to_path ".", false
in
- d ^ if vis then "/frama-c" else "/.frama-c"
+ Fc_Filepath.Normalized.concat
+ d (if vis then "frama-c" else ".frama-c")
]
let visible_ref = !config_visible_ref
end)
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 4fd6bf083a0f5e51bc3497d12e1ab68fa7cc5042..bab956df2dcfd4ed2ddb63ee051791f7d7e5df27 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -186,10 +186,10 @@ val positive_debug_ref: int ref
(** @since Boron-20100401 *)
val session_is_set_ref: (unit -> bool) ref
-val session_ref: (unit -> string) ref
+val session_ref: (unit -> Filepath.Normalized.t) ref
val config_is_set_ref: (unit -> bool) ref
-val config_ref: (unit -> string) ref
+val config_ref: (unit -> Filepath.Normalized.t) ref
(**/**)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index bbd3f32cad03a385d96ae915dd67eec499489429..81dd5d8eff799578387253afebeff39a9592a2f7 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -171,7 +171,7 @@ let symbolic_dirs = Hashtbl.create 3
let add_symbolic_dir name dir =
Hashtbl.replace symbolic_dirs name dir;
- (insert cwd dir).symbolic_name <- Some name
+ (insert cwd (dir:>string)).symbolic_name <- Some name
let reset_symbolic_dirs () = Hashtbl.clear symbolic_dirs
@@ -260,6 +260,7 @@ module Normalized = struct
let of_string ?existence ?base_name s = normalize ?existence ?base_name s
let concat ?existence t s = normalize ?existence (t ^ "/" ^ s)
let to_pretty_string s = pretty s
+ let to_string_list l = l
let equal : t -> t -> bool = (=)
let compare = String.compare
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 935d89611afc2294cc10c10d25836f3c5414681b..e9ebe88cb45f396220e39092253b5eccc82afbc2 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -61,12 +61,6 @@ val normalize: ?existence:existence -> ?base_name:string -> string -> string
@since Aluminium-20160501 *)
val relativize: ?base_name:string -> string -> string
-(** returns true if the file is relative to [base]
- (that is, it is prefixed by [base_name]), or to the current
- working directory if no base is specified.
- @since Aluminium-20160501 *)
-val is_relative: ?base_name:string -> string -> bool
-
(** DEPRECATED: use [Normalized.to_pretty_string] instead.
Pretty-print a path according to these rules:
- relative filenames are kept, except for leading './', which are stripped;
@@ -83,23 +77,6 @@ val is_relative: ?base_name:string -> string -> bool
val pretty: string -> string
[@@deprecated "Use Filepath.Normalized.to_pretty_string instead."]
-(** [add_symbolic_dir name dir] indicates that the (absolute) path [dir] must
- be replaced by [name] when pretty-printing paths.
- This alias ensures that system-dependent paths such as FRAMAC_SHARE are
- printed identically in different machines. *)
-val add_symbolic_dir: string -> string -> unit
-
-(** Remove all symbolic dirs that have been added earlier.
- @since Frama-C+dev *)
-val reset_symbolic_dirs: unit -> unit
-
-(** Returns the list of symbolic dirs added via [add_symbolic_dir], plus
- preexisting ones (e.g. FRAMAC_SHARE), as pairs (name, dir).
-
- @since 22.0-Titanium
-*)
-val all_symbolic_dirs: unit -> (string * string) list
-
(** The [Normalized] module is simply a wrapper that ensures that paths are
always normalized. Used by [Datatype.Filepath].
@since 18.0-Argon *)
@@ -129,6 +106,12 @@ module Normalized: sig
See [pretty] for details about usage. *)
val to_pretty_string: t -> string
+ (** [to_string_list l] returns [l] as a list of strings containing the
+ absolute paths to the elements of [l].
+ @since Frama-C+dev
+ *)
+ val to_string_list: t list -> string list
+
val equal: t -> t -> bool
(** Compares normalized paths *)
@@ -199,6 +182,31 @@ module Normalized: sig
val to_base_uri: t -> string option * string
end
+(** returns true if the file is relative to [base]
+ (that is, it is prefixed by [base_name]), or to the current
+ working directory if no base is specified.
+ @since Aluminium-20160501
+ @modify Frama-C+dev argument types changed from string to Normalized.t
+*)
+val is_relative: ?base_name:Normalized.t -> Normalized.t -> bool
+
+(** [add_symbolic_dir name dir] indicates that the (absolute) path [dir] must
+ be replaced by [name] when pretty-printing paths.
+ This alias ensures that system-dependent paths such as FRAMAC_SHARE are
+ printed identically in different machines. *)
+val add_symbolic_dir: string -> Normalized.t -> unit
+
+(** Remove all symbolic dirs that have been added earlier.
+ @since Frama-C+dev *)
+val reset_symbolic_dirs: unit -> unit
+
+(** Returns the list of symbolic dirs added via [add_symbolic_dir], plus
+ preexisting ones (e.g. FRAMAC_SHARE), as pairs (name, dir).
+
+ @since 22.0-Titanium
+*)
+val all_symbolic_dirs: unit -> (string * Normalized.t) list
+
(** Describes a position in a source file.
@since 18.0-Argon
*)
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index d29eb062dfc7511d8298b2371658f78012199247..5a9c80fef4174e1a1d6a58cd30f9aacae8e72fd9 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1825,8 +1825,8 @@ class main_window () : main_window_extension_points =
end
let make_splash () =
- GMain.Rc.add_default_file (Fc_config.datadir ^"/frama-c.rc");
- GMain.Rc.add_default_file (Fc_config.datadir ^"/frama-c-user.rc");
+ GMain.Rc.add_default_file ((Fc_config.datadir:>string) ^"/frama-c.rc");
+ GMain.Rc.add_default_file ((Fc_config.datadir:>string) ^"/frama-c-user.rc");
(*print_endline ("BOOT: " ^ (Glib.Main.setlocale `ALL None));*)
let (_:string) = GtkMain.Main.init ~setlocale:false () in
(*print_endline ("START: " ^ (Glib.Main.setlocale `ALL None));*)
diff --git a/src/plugins/gui/filetree.ml b/src/plugins/gui/filetree.ml
index a0be9aeb2d40cc93e900292886fcb52c53dbce41..7dbc3973b988555cdc734144379c11067bd03304 100644
--- a/src/plugins/gui/filetree.ml
+++ b/src/plugins/gui/filetree.ml
@@ -293,7 +293,8 @@ module MYTREE = struct
Cil.hasAttribute "FC_BUILTIN" (Cil_datatype.Global.attr g)
let comes_from_share filename =
- Filepath.is_relative ~base_name:Fc_config.datadir filename
+ let path = Filepath.Normalized.of_string filename in
+ Filepath.is_relative ~base_name:Fc_config.datadir path
let is_function t = match t with
| MFile _ -> false
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index a4339a28ec8f1e5cd250eb1c35cf518a9dad3abd..911baf29bf37751d3a1ac0fbe28a0a9c570fa2b7 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -24,14 +24,15 @@
let () =
begin
- Wutil.share := Fc_config.datadir;
+ Wutil.share := (Fc_config.datadir :> string);
Wutil.flush := (fun msg -> Gui_parameters.warning "%s" msg);
end
let framac_logo, framac_icon =
try
let img ext =
- Some (GdkPixbuf.from_file (Fc_config.datadir ^ "/frama-c." ^ ext))
+ Some (GdkPixbuf.from_file
+ ((Fc_config.datadir:>string) ^ "/frama-c." ^ ext))
in
img "png", img "ico"
with
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 62ee563dbe9f07043c858439d9daab6353bd2304..fc33b7542ff6d3b3d37335fed4c740d0ee1afc02 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -250,7 +250,12 @@ let gen_run remarks =
let taxonomies = [ToolComponent.create ~name ~rules ()] in
let results = results @ user_annot_results in
let artifacts = gen_artifacts () in
- let uriBases = ("PWD", Sys.getcwd ()) :: Filepath.all_symbolic_dirs () in
+ let symbolicDirs =
+ List.map (fun (key, (dir : Filepath.Normalized.t)) ->
+ (key, (dir :> string))
+ ) (Filepath.all_symbolic_dirs ())
+ in
+ let uriBases = ("PWD", Sys.getcwd ()) :: symbolicDirs in
let uriBasesJson =
List.fold_left (fun acc (name, dir) ->
let baseUri =
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index acc91d128b903d2e83c8276b410346effc5fb6d3..effed249b3a61a1e1df9ae2dafdf7830f55c9083 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -53,9 +53,12 @@ let () =
signature
begin fun rq () ->
set_version rq Fc_config.version ;
- set_datadir rq Fc_config.datadir ;
- set_libdir rq Fc_config.libdir ;
- set_pluginpath rq Fc_config.plugin_dir ;
+ set_datadir rq (Fc_config.datadir :> string) ;
+ set_libdir rq (Fc_config.libdir :> string) ;
+ let pluginpath =
+ Filepath.Normalized.to_string_list Fc_config.plugin_dir
+ in
+ set_pluginpath rq pluginpath ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index 5acf76ffc994df47c00934d36bd454911dbb74e2..d771ebc636d35f93ca864c081da3eec1815660de 100644
--- a/src/plugins/server/package.ml
+++ b/src/plugins/server/package.ml
@@ -382,9 +382,9 @@ let resolve_readme ~plugin = function
let file =
match plugin with
| Kernel ->
- Printf.sprintf "%s/server/%s" Fc_config.datadir readme
+ Printf.sprintf "%s/server/%s" (Fc_config.datadir:>string) readme
| Plugin name ->
- Printf.sprintf "%s/%s/server/%s" Fc_config.datadir name readme
+ Printf.sprintf "%s/%s/server/%s" (Fc_config.datadir:>string) name readme
in Some file
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 206ebd4ca538956d506237e164f49b170773b16e..3bc8bae5c264c3a96f091ad8b8cb644d881c70a5 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -95,7 +95,7 @@ let publish ~page ?name ?(index=[]) ~title
page.sections <- section :: page.sections ; href
let protocole ~title ~readme:filename =
- let readme = Printf.sprintf "%s/server/%s" Fc_config.datadir filename in
+ let readme = Printf.sprintf "%s/server/%s" (Fc_config.datadir :> string) filename in
ignore (page `Protocol ~title ~readme ~filename ())
let () = protocole ~title:"Architecture" ~readme:"server.md"
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 5f571b6d2de43b264e2da334157e750bf5227ea9..0aa7507ffd1a8c58911dbfd3200e7fef3072b03e 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -147,7 +147,7 @@ let warn_builtin_override kf source bname =
let internal =
(* TODO: treat this 'internal' *)
let file = source.Filepath.pos_path in
- Filepath.is_relative ~base_name:Fc_config.datadir (file :> string)
+ Filepath.is_relative ~base_name:Fc_config.datadir file
in
if Kernel_function.is_definition kf && not internal
then
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index d78a8601b1a5a5120ce24da68e4d4d48f88f2ff2..7262bebbeaf75a657a269943b180fd73499022fe 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -99,8 +99,9 @@ let warn_unsupported_spec name =
Value_parameters.warning ~once:true ~current:true
~wkey:Value_parameters.wkey_libc_unsupported_spec
"@[The specification of function '%s' is currently not supported by Eva.@ \
- Consider adding %s@ to the analyzed source files.@]"
- name (Fc_config.datadir ^ "/libc/" ^ header)
+ Consider adding '%a'@ to the analyzed source files.@]"
+ name Filepath.Normalized.pretty
+ (Filepath.Normalized.concat Fc_config.framac_libc header)
with Not_found -> ()
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index bd90f0d1795fcc69eed0efada0cc924598649f2d..00b5815d2cd892a51bd9ea4d3a27588998b47e0c 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1177,7 +1177,7 @@ let base_output () =
| dir ->
make_output_dir dir ; dir in
base_output := Some output;
- Fc_Filepath.add_symbolic_dir "WPOUT" output ;
+ Fc_Filepath.(add_symbolic_dir "WPOUT" (Normalized.of_string output)) ;
Datatype.Filepath.of_string output
| Some output -> Datatype.Filepath.of_string output
diff --git a/tests/libc/check_compliance.ml b/tests/libc/check_compliance.ml
index 978fd6574cad91d274e209449d05983a938717a7..3fab55c7989fe06a0dd332dafeb7f3bb9c6c47d8 100644
--- a/tests/libc/check_compliance.ml
+++ b/tests/libc/check_compliance.ml
@@ -88,7 +88,7 @@ let () =
let vis = new stdlib_visitor in
ignore (Visitor.visitFramacFile (vis :> Visitor.frama_c_visitor) (Ast.get ()));
let fc_stdlib_idents = vis#get_idents in
- let dir = Filename.concat Fc_config.datadir "compliance" in
+ let dir = Filename.concat (Fc_config.datadir:>string) "compliance" in
let c11_idents = Json.(to_table HeadersOnly (parse dir "c11_functions.json"))
and c11_headers = Json.(to_set (parse dir "c11_headers.json"))
and glibc_idents = Json.(to_set (parse dir "glibc_functions.json"))
diff --git a/tests/libc/oracle/string_h.res.oracle b/tests/libc/oracle/string_h.res.oracle
index fd2eaee19bf54f636ccc83358a1c4dc259534597..694c2eca6d343c4e01bd0f49cd4dff2a4221be53 100644
--- a/tests/libc/oracle/string_h.res.oracle
+++ b/tests/libc/oracle/string_h.res.oracle
@@ -237,7 +237,7 @@
[eva] using specification for function strdup
[eva:libc:unsupported-spec] tests/libc/string_h.c:146: Warning:
The specification of function 'strdup' is currently not supported by Eva.
- Consider adding ./share/libc/string.c to the analyzed source files.
+ Consider adding 'share/libc/string.c' to the analyzed source files.
[eva] tests/libc/string_h.c:146: Warning: ignoring unsupported \allocates clause
[eva] tests/libc/string_h.c:146:
function strdup: precondition 'valid_string_s' got status valid.
@@ -247,7 +247,7 @@
[eva] using specification for function strndup
[eva:libc:unsupported-spec] tests/libc/string_h.c:147: Warning:
The specification of function 'strndup' is currently not supported by Eva.
- Consider adding ./share/libc/string.c to the analyzed source files.
+ Consider adding 'share/libc/string.c' to the analyzed source files.
[eva] tests/libc/string_h.c:147: Warning: ignoring unsupported \allocates clause
[eva] tests/libc/string_h.c:147:
function strndup: precondition 'valid_string_s' got status valid.
diff --git a/tests/misc/filepath_test.ml b/tests/misc/filepath_test.ml
index e55e4bd028458e6603ac8122437a8bbc76648349..078197d73b9927f9921d4547e01e7ddeb5c4f69b 100644
--- a/tests/misc/filepath_test.ml
+++ b/tests/misc/filepath_test.ml
@@ -17,7 +17,7 @@ let () =
(Filepath.relativize "./tests/..");
Kernel.feedback "relativize(/a/bc/d,base_name:/a/b/): %s"
(Filepath.relativize ~base_name:"/a/b/" "/a/bc/d");
- Filepath.add_symbolic_dir "SYMB" "/tmp/symb/";
+ Filepath.add_symbolic_dir "SYMB" (Filepath.Normalized.of_string "/tmp/symb/");
Kernel.feedback "pretty with symbolic path: %a"
Filepath.Normalized.pretty
(Filepath.Normalized.of_string "/tmp/symb/file.c")
diff --git a/tests/syntax/oracle/cpp-command.0.res.oracle b/tests/syntax/oracle/cpp-command.0.res.oracle
index f910fe5ece81818d84c0dab9a4af138213c8ffa8..de97d8b46568dffe05790ad4c4c8f3092eef2b13 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] [-Ishare/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 4d07269a88da2aca64a17efaba30377dfd8fcaab..4d18c0807800d67edd1d125280ca266d00ea1387 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 = -Ishare/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 2f8d187fc5edca6bf9ef78bff98609317dc67759..72c1b47b58cfe45589c126742720883c74e3d442 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. -Ishare/libc -D__FRAMAC__ -D__FC_MACHDEP_X86_32 -dD -nostdinc 'tests/syntax/cpp-command.c' -o 'TMPDIR/FILE.i'