diff --git a/bin/migration_scripts/titanium2vanadium.sh b/bin/migration_scripts/titanium2vanadium.sh
index 7c1b304029c0cd6c2c7dea0ef5dd0839405707c4..4288a6b24f61cb03d2e82b11beb154e826b1be86 100755
--- a/bin/migration_scripts/titanium2vanadium.sh
+++ b/bin/migration_scripts/titanium2vanadium.sh
@@ -106,7 +106,9 @@ process_file ()
-e 's/Extlib\.the \([^~]\)/Option.get \1/g' \
-e 's/Extlib\.opt_equal/Option.equal/g' \
-e 's/Extlib\.opt_compare/Option.compare/g' \
- -e 's/Extlib\.array_exists/Array.exists/g'
+ -e 's/Extlib\.array_exists/Array.exists/g' \
+ -e 's/Filepath\.Normalized\.is_unknown/Filepath.Normalized.is_empty/g' \
+ -e 's/Filepath\.Normalized\.unknown/Filepath.Normalized.empty/g'
}
apply_one_dir ()
diff --git a/share/analysis-scripts/list_functions.ml b/share/analysis-scripts/list_functions.ml
index 96511af9c7140a248de0dd7fbe157e2f70f05887..4bf75dc70a1bb9763f12f18e9c7c03d695cebd2d 100644
--- a/share/analysis-scripts/list_functions.ml
+++ b/share/analysis-scripts/list_functions.ml
@@ -282,7 +282,7 @@ let run () =
(fun fi1 fi2 -> Extlib.compare_ignore_case fi1.name fi2.name) funinfos
in
let outfp = Output.get () in
- if Filepath.Normalized.is_unknown outfp then
+ if Filepath.Normalized.is_empty outfp then
print_text funinfos
else
let funinfos_json = `List (List.map (fun fi ->
diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index fd23b4bec48a74b72bd789d3b2f5df3bce4af279..e0edf8abfab073a2744df8bb1db580eae191c358 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -87,8 +87,8 @@ let () =
(* Load Frama-c from disk if required *)
let load_binary () =
- let filepath = Kernel.LoadState.get () in
- if filepath <> Filepath.Normalized.unknown then begin
+ if not (Kernel.LoadState.is_empty ()) then begin
+ let filepath = Kernel.LoadState.get () in
try
Project.load_all filepath
with Project.IOError s ->
@@ -133,8 +133,8 @@ let () = Extlib.safe_at_exit time
(* Save Frama-c on disk if required *)
let save_binary error_extension =
- let filename = Kernel.SaveState.get () in
- if not (Filepath.Normalized.is_unknown filename) then begin
+ if not (Kernel.SaveState.is_empty ()) then begin
+ let filename = Kernel.SaveState.get () in
Kernel.SaveState.clear ();
let realname =
match error_extension with
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index e818857a279b7482830c58d6473fd2d73b6b910b..60f93f7bb1b8c480cf391f4ef18f14c4ae95bd1f 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -606,7 +606,7 @@ and pp_location fmt (pos_start,pos_end) =
and pp_if_loc_known prefix suffix fmt loc =
if print_locations &&
- not (Filepath.Normalized.is_unknown (fst loc).Filepath.pos_path)
+ not (Filepath.Normalized.is_empty (fst loc).Filepath.pos_path)
then Format.fprintf fmt "%s%a%s" prefix pp_location loc suffix
else ()
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 6cd0cc0cecf3212337ddc80ec4ea9b66baa0ffb8..5198bfd3bd84f2e329605ac89e0f03fe86a9b46a 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -53,9 +53,9 @@ module D =
type t = file
let name = "File"
let reprs =
- [ NeedCPP(Filepath.Normalized.unknown, "", [], Unknown);
- NoCPP Filepath.Normalized.unknown;
- External(Filepath.Normalized.unknown, "")
+ [ NeedCPP(Filepath.Normalized.empty, "", [], Unknown);
+ NoCPP Filepath.Normalized.empty;
+ External(Filepath.Normalized.empty, "")
]
let structural_descr = Structural_descr.t_abstract
let mem_project = Datatype.never_any_project
@@ -1744,17 +1744,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;
- let audit_check_path = Kernel.AuditCheck.get () in
- if not (Filepath.Normalized.is_unknown audit_check_path) then begin
+ if not (Kernel.AuditCheck.is_empty ()) then begin
let all_sources_tbl = compute_sources_table cpp_commands in
- let expected_hashes = source_hashes_of_json audit_check_path in
+ let expected_hashes = source_hashes_of_json (Kernel.AuditCheck.get ()) in
check_source_hashes expected_hashes all_sources_tbl
end;
- let audit_path = Kernel.AuditPrepare.get () in
- if not (Filepath.Normalized.is_unknown audit_path) then begin
+ if not (Kernel.AuditPrepare.is_empty ()) 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/ast_queries/json_compilation_database.ml b/src/kernel_services/ast_queries/json_compilation_database.ml
index 895e3e49c46f2d187dfa05300cd47e3dd1fb63a3..11c2802451cd21e4e895e0d32639d3a8ce2e1a34 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ml
@@ -270,7 +270,7 @@ let compute_flags_from_file () =
Flags.mark_as_computed ()
let get_flags f =
- if not (Filepath.Normalized.is_unknown (Kernel.JsonCompilationDatabase.get ())) then begin
+ if not (Kernel.JsonCompilationDatabase.is_empty ()) then begin
if not (Flags.is_computed ()) then compute_flags_from_file ();
try
let flags = Flags.find f in
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index e3b4f91162884ed8c60721538f0894870123e7db..53e2eb4f2c981701a6a7956b3942232c94a0a8b6 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -480,7 +480,7 @@ struct
(struct
include Datatype.Filepath
include X
- let default () = Filepath.Normalized.unknown
+ let default () = Filepath.Normalized.empty
let functor_name = "Filepath"
end)
@@ -532,6 +532,7 @@ struct
else
p
+ let is_empty () = Filepath.Normalized.is_empty (get ())
end
(* ************************************************************************ *)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index f4ce284ef09a4f137820680f724dc74bd7445433..4d16f3101e799b36e4bad457557a6fbf44c31db1 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -293,7 +293,16 @@ module type With_output = sig
end
(** signature for normalized pathnames. *)
-module type Filepath = S with type t = Filepath.Normalized.t
+module type Filepath = sig
+ include S with type t = Filepath.Normalized.t
+
+ (**
+ Whether the Filepath is empty.
+
+ @since Frama-C+dev
+ *)
+ val is_empty: unit -> bool
+end
(** signature for searching files in a specific directory. *)
module type Specific_dir = sig
diff --git a/src/libraries/datatype/datatype.ml b/src/libraries/datatype/datatype.ml
index 774bdb8c79216b030a31e7f4f69f65aa0eaa0a41..2ed442511ec751e1cf1ab471985351979b19a40f 100644
--- a/src/libraries/datatype/datatype.ml
+++ b/src/libraries/datatype/datatype.ml
@@ -1946,7 +1946,7 @@ module Filepath = struct
let pretty = Filepath.Normalized.pretty
let varname _ = "p"
end)
- let dummy = Filepath.Normalized.unknown
+ let dummy = Filepath.Normalized.empty
let of_string ?existence ?base_name s =
Filepath.Normalized.of_string ?existence ?base_name s
let concat ?existence t s = Filepath.Normalized.concat ?existence t s
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index f68bcdc4bcac40f3e2341aa53322808397f3c22a..b9400c45d0cc06b881dde52b477fbfd984fc0187 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -829,7 +829,7 @@ let create_by_copy
module Undo = struct
let short_filename = "frama_c_undo_restore"
- let filename = ref Filepath.Normalized.unknown
+ let filename = ref Filepath.Normalized.empty
let clear_breakpoint () = Extlib.safe_remove (!filename:>string)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 567261e3b48b51525b1a55d9ff5cf9b4b9b86c2e..bbd3f32cad03a385d96ae915dd67eec499489429 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -269,8 +269,10 @@ module Normalized = struct
if case_sensitive then String.compare s1 s2
else Extlib.compare_ignore_case s1 s2
- let unknown = normalize ""
- let is_unknown fp = equal fp unknown
+ let empty = normalize ""
+ let unknown = empty
+ let is_empty fp = equal fp empty
+ let is_unknown = is_empty
let special_stdout = normalize "-"
let is_special_stdout fp = equal fp special_stdout
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 72577230acf4a7e9924fda47ada63639a2d0fda3..935d89611afc2294cc10c10d25836f3c5414681b 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -154,11 +154,25 @@ module Normalized: sig
(** Pretty-prints the normalized (absolute) path. *)
val pp_abs: Format.formatter -> t -> unit
- (** Unknown filepath, used as 'dummy' for [Datatype.Filepath]. *)
+ (** Unknown filepath, used as 'dummy' for [Datatype.Filepath].
+ @deprecated Frama-C+dev use 'empty' instead
+ *)
val unknown: t
+ [@@alert deprecated "Use Filepath.Normalized.empty instead"]
- (** @since 20.0-Calcium *)
+ (** @since 20.0-Calcium
+ @deprecated Frama-C+dev use 'is_empty' instead
+ *)
val is_unknown: t -> bool
+ [@@alert deprecated "Use Filepath.Normalized.is_empty instead"]
+
+ (** Empty filepath, used as 'dummy' for [Datatype.Filepath].
+ @since Frama-C+dev.
+ *)
+ val empty: t
+
+ (** @since Frama-C+dev *)
+ val is_empty: t -> bool
(** [is_special_stdout f] returns [true] iff [f] is '-' (a single dash),
which is a special notation for 'stdout'.
diff --git a/src/plugins/aorai/aorai_option.ml b/src/plugins/aorai/aorai_option.ml
index 02127aa546d10d2cbffa57589840ca4a46c0f47b..c047a144ab9d47b2b9749e6c6681933971d9c277 100644
--- a/src/plugins/aorai/aorai_option.ml
+++ b/src/plugins/aorai/aorai_option.ml
@@ -173,7 +173,7 @@ let is_on () =
Buchi.is_default () && Ya.is_default () )
let promela_file () =
- if Fc_Filepath.Normalized.is_unknown (Buchi.get ()) then To_Buchi.get () else Buchi.get ()
+ if not (Buchi.is_empty ()) then Buchi.get () else To_Buchi.get ()
let advance_abstract_interpretation () =
not (AbstractInterpretationOff.get ()) && not (AbstractInterpretation.get ())
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index ec4f9e123cd8b6f1056b5e56e023becf30c9b68e..90965ec6c8d0c7b65f453ead13e1aaa07f536169 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -27,12 +27,12 @@ open Logic_ptree
open Promelaast
(* [VP] Need to get rid of those global references at some point. *)
-let promela_file = ref Filepath.Normalized.unknown
-let c_file = ref Filepath.Normalized.unknown
-let output_c_file = ref Filepath.Normalized.unknown
-let ltl_tmp_file = ref Filepath.Normalized.unknown
-let ltl_file = ref Filepath.Normalized.unknown
-let dot_file = ref Filepath.Normalized.unknown
+let promela_file = ref Filepath.Normalized.empty
+let c_file = ref Filepath.Normalized.empty
+let output_c_file = ref Filepath.Normalized.empty
+let ltl_tmp_file = ref Filepath.Normalized.empty
+let ltl_file = ref Filepath.Normalized.empty
+let dot_file = ref Filepath.Normalized.empty
let ltl2ba_params = " -l -p -o "
let ltl_to_promela = Hashtbl.create 7
@@ -178,14 +178,14 @@ let init_file_names () =
in
Filepath.Normalized.of_string name
in
- if Filepath.Normalized.is_unknown (Aorai_option.Ya.get ()) then
- if Filepath.Normalized.is_unknown (Aorai_option.Buchi.get ()) then begin
+ if Aorai_option.Ya.is_empty () then
+ if Aorai_option.Buchi.is_empty () then begin
(* ltl_file name is given and has to point out a valid file. *)
ltl_file := Aorai_option.Ltl_File.get ();
if Aorai_option.Dot.get() then dot_file := freshname !ltl_file ".dot";
(* The LTL file is always used. *)
(* The promela file can be given or not. *)
- if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) then begin
+ if not (Aorai_option.To_Buchi.is_empty ()) then begin
ltl_tmp_file:=
freshname (Aorai_option.promela_file ()) ".ltl";
promela_file:= Aorai_option.promela_file ();
@@ -203,8 +203,7 @@ let init_file_names () =
Extlib.cleanup_at_exit (!promela_file :> string);
end
end else begin
- if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) &&
- not (Filepath.Normalized.is_unknown (Aorai_option.Ltl_File.get ()))
+ if not (Aorai_option.To_Buchi.is_empty ()) && not (Aorai_option.Ltl_File.is_empty ())
then begin
Aorai_option.abort
"Error. '-buchi' option is incompatible with '-to-buchi' and '-ltl' \
@@ -217,12 +216,10 @@ let init_file_names () =
dot_file := freshname !promela_file ".dot";
end
else begin
- let ya_file = Aorai_option.Ya.get () in
- if (Filepath.Normalized.is_unknown ya_file) then
- Aorai_option.abort
- "invalid Ya file name %a" Filepath.Normalized.pretty ya_file;
+ if Aorai_option.Ya.is_empty () then
+ Aorai_option.abort "empty Ya file name";
if Aorai_option.Dot.get() then
- dot_file := freshname ya_file ".dot"
+ dot_file := freshname (Aorai_option.Ya.get ()) ".dot"
end;
display_status ()
@@ -243,8 +240,8 @@ let work () =
let file = Ast.get () in
Aorai_utils.initFile file;
printverb "C file loading : done\n";
- if Filepath.Normalized.is_unknown (Aorai_option.Ya.get ()) then
- if Filepath.Normalized.is_unknown (Aorai_option.Buchi.get ()) then begin
+ if Aorai_option.Ya.is_empty () then
+ if Aorai_option.Buchi.is_empty () then begin
ltl_to_ltlLight !ltl_file !ltl_tmp_file;
printverb "LTL loading : done\n";
let cmd = Format.asprintf "ltl2ba %s -F %a > %a"
@@ -255,16 +252,16 @@ let work () =
Aorai_option.abort "failed to run: %s" cmd ;
printverb "LTL ~> Promela (ltl2ba): done\n"
end;
- if not (Filepath.Normalized.is_unknown (Aorai_option.To_Buchi.get ())) then
+ if not (Aorai_option.To_Buchi.is_empty ()) then
printverb ("Finished.\nGenerated file: '"^(Filepath.Normalized.to_pretty_string !promela_file)^"'\n")
else
begin
(* Step 3 : Loading promela_file and checking the consistency between informations from C code and LTL property *)
(* Such as functions name and global variables. *)
- if not (Filepath.Normalized.is_unknown (Aorai_option.Buchi.get ())) then
+ if not (Aorai_option.Buchi.is_empty ()) then
load_promela_file_withexps !promela_file
- else if not (Filepath.Normalized.is_unknown (Aorai_option.Ya.get ())) then
+ else if not (Aorai_option.Ya.is_empty ()) then
load_ya_file (Aorai_option.Ya.get ())
else
load_promela_file !promela_file;
diff --git a/src/plugins/callgraph/Callgraph.mli b/src/plugins/callgraph/Callgraph.mli
index 0d649136073dd5b2302303f3db77b9f2bae279aa..e7ba902325e6c84043bec088f00613e614853015 100644
--- a/src/plugins/callgraph/Callgraph.mli
+++ b/src/plugins/callgraph/Callgraph.mli
@@ -23,7 +23,7 @@
(** Callgraph plugin. *)
module Options: sig
- module Filename: Parameter_sig.String
+ module Filename: Parameter_sig.Filepath
module Service_roots: Parameter_sig.Kernel_function_set
module Uncalled: Parameter_sig.Bool
module Uncalled_leaf: Parameter_sig.Bool
diff --git a/src/plugins/callgraph/options.ml b/src/plugins/callgraph/options.ml
index d42856664a9fe2f3e6bc2d0124c99ae90e729a68..04158a6a507d274ce7cedc76f220e6da4170279f 100644
--- a/src/plugins/callgraph/options.ml
+++ b/src/plugins/callgraph/options.ml
@@ -32,10 +32,12 @@ include
end)
module Filename =
- Empty_string
+ Filepath
(struct
let option_name = "-cg"
let arg_name = "filename"
+ let file_kind = "DOT"
+ let existence = Fc_Filepath.Indifferent
let help = "dump the callgraph to the file \
<filename> in dot format"
end)
@@ -97,9 +99,10 @@ module Uncalled_leaf =
let dump output g =
let file = Filename.get () in
- feedback ~level:2 "dumping the graph into file %s" file;
+ feedback ~level:2 "dumping the graph into file %a"
+ Fc_Filepath.Normalized.pretty file;
try
- let cout = open_out file in
+ let cout = open_out (file:>string) in
output cout g;
close_out cout
with e ->
diff --git a/src/plugins/callgraph/options.mli b/src/plugins/callgraph/options.mli
index aa6fd2e5026a828c84f95be2cbca523154793c72..ab238a90b57d79c2387e9f5e9e688c2779d2d35c 100644
--- a/src/plugins/callgraph/options.mli
+++ b/src/plugins/callgraph/options.mli
@@ -23,7 +23,7 @@
include Plugin.S
val name: string
-module Filename: Parameter_sig.String
+module Filename: Parameter_sig.Filepath
module Roots: Parameter_sig.Kernel_function_set
module Service_roots: Parameter_sig.Kernel_function_set
module Function_pointers: Parameter_sig.Bool
diff --git a/src/plugins/callgraph/register.ml b/src/plugins/callgraph/register.ml
index d7da576b50f9ee45167f7e3404d27e0c179facd8..487f6d51055e43009da0df956a6e071653fd135d 100644
--- a/src/plugins/callgraph/register.ml
+++ b/src/plugins/callgraph/register.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
let main () =
- if Options.Filename.get () <> "" then
+ if not (Options.Filename.is_empty ()) then
if Options.Services.get () then begin
if not (Services.is_computed ()) then Services.dump ()
end else
diff --git a/src/plugins/dive/main.ml b/src/plugins/dive/main.ml
index 7387399121640d369c24df0f3323af284fe4c709..10d3da3b178ed82ae91cff195a264c333b5072ef 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -22,13 +22,13 @@
type format = Dot | Json
-let output format context basename =
- let filename, output_function = match format with
- | Dot -> basename ^ ".dot", Dive_graph.ouptput_to_dot
- | Json -> basename ^ ".json", Dive_graph.ouptput_to_json
+let output format context filename =
+ let output_function = match format with
+ | Dot -> Dive_graph.ouptput_to_dot
+ | Json -> Dive_graph.ouptput_to_json
in
- Self.result "output to %s" filename;
- let out_channel = open_out filename in
+ Self.result "output to %a" Filepath.Normalized.pretty filename;
+ let out_channel = open_out (filename:>string) in
output_function out_channel (Context.get_graph context);
close_out out_channel
@@ -57,9 +57,9 @@ let main () =
if not (Self.FromFunctionAlarms.is_empty ()) then
Alarms.iter add_alarm;
(* Output it *)
- if Self.OutputDot.get () <> "" then
+ if not (Self.OutputDot.is_empty ()) then
output Dot context (Self.OutputDot.get ());
- if Self.OutputJson.get () <> "" then
+ if not (Self.OutputJson.is_empty ()) then
output Json context (Self.OutputJson.get ());
end
diff --git a/src/plugins/dive/self.ml b/src/plugins/dive/self.ml
index 26a925a3f5475acf84c842e7a8cb0b1ae10672ff..ba3fd755c8f3bf66b9fe0aa6d90141d7dbb9b181 100644
--- a/src/plugins/dive/self.ml
+++ b/src/plugins/dive/self.ml
@@ -29,18 +29,22 @@ include Plugin.Register
let help = "An interactive imprecision graph generator for Eva."
end)
-module OutputDot = Empty_string
+module OutputDot = Filepath
(struct
let option_name = "-dive-output-dot"
- let help = "Outputs the built graph into a dot file with this basename."
- let arg_name = "basename"
+ let arg_name = "output.dot"
+ let file_kind = "DOT"
+ let existence = Fc_Filepath.Indifferent
+ let help = "Outputs the built graph in DOT format to the specified file."
end)
-module OutputJson = Empty_string
+module OutputJson = Filepath
(struct
let option_name = "-dive-output-json"
- let help = "Outputs the built graph into a json file with this basename."
- let arg_name = "basename"
+ let arg_name = "output.json"
+ let file_kind = "JSON"
+ let existence = Fc_Filepath.Indifferent
+ let help = "Outputs the built graph in JSON format to the specified."
end)
module DepthLimit = Int
diff --git a/src/plugins/dive/self.mli b/src/plugins/dive/self.mli
index cb5014982463f0f11c2adc18224bcc0c5ef1ea47..664546c1cc6887e6ac3a71182c88731e1a6e8eec 100644
--- a/src/plugins/dive/self.mli
+++ b/src/plugins/dive/self.mli
@@ -26,8 +26,8 @@ module type Varinfo_set = Parameter_sig.Set
with type elt = Cil_types.varinfo
and type t = Cil_datatype.Varinfo.Set.t
-module OutputDot : Parameter_sig.String
-module OutputJson : Parameter_sig.String
+module OutputDot : Parameter_sig.Filepath
+module OutputJson : Parameter_sig.Filepath
module DepthLimit : Parameter_sig.Int
module FromFunctionAlarms : Parameter_sig.Kernel_function_set
module FromBases : Varinfo_set
diff --git a/src/plugins/dive/tests/test_config b/src/plugins/dive/tests/test_config
index 9ff9387337545ed97c88920ed5c79a722351eaa8..b5de8cfbedf81997ee828999794f2b0c93025bed 100644
--- a/src/plugins/dive/tests/test_config
+++ b/src/plugins/dive/tests/test_config
@@ -1,3 +1,3 @@
LOG: @PTEST_NAME@.dot
-OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope,dive -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output-dot @PTEST_RESULT@/@PTEST_NAME@
+OPT: -no-autoload-plugins -load-module from,inout,eva,variadic,scope,dive -check -eva-msg-key=-initial-state -eva-no-show-progress -dive-output-dot @PTEST_RESULT@/@PTEST_NAME@.dot
FILTER: perl -0777 -pe 's/\[server[^[]*//g'
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index dc212069f0d533bf8513d4311ccaf8ef7f9daaa7..b8a09ed3b99df3c6f9b02ba4b5bb1b5bb427c4a4 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -554,13 +554,14 @@ let gen_alarms env =
gen_section_postlude env
let mk_remarks is_draft =
- let f = Mdr_params.Remarks.get () in
- if f <> "" then Parse_remarks.get_remarks f
+ if not (Mdr_params.Remarks.is_empty ()) then
+ Parse_remarks.get_remarks (Mdr_params.Remarks.get ())
else if is_draft then begin
let f = Mdr_params.Output.get() in
- if Sys.file_exists f then begin
+ if Sys.file_exists (f:>string) then begin
Mdr_params.feedback
- "Re-using pre-existing remarks in draft file %s" f;
+ "Re-using pre-existing remarks in draft file %a"
+ Filepath.Normalized.pretty f;
Parse_remarks.get_remarks f
end else Datatype.String.Map.empty
end else Datatype.String.Map.empty
@@ -609,8 +610,9 @@ let gen_report ~draft:is_draft () =
let doc = Markdown.pandoc ~title ~authors ?date elements in
let file = Mdr_params.Output.get() in
try
- Command.print_file file (fun fmt -> Markdown.pp_pandoc fmt doc) ;
- Mdr_params.result "Report %s generated" file
+ Command.print_file (file:>string) (fun fmt -> Markdown.pp_pandoc fmt doc) ;
+ Mdr_params.result "Report %a generated" Filepath.Normalized.pretty file
with Sys_error s ->
Mdr_params.warning
- "Unable to open %s for writing (%s). No report generated" file s
+ "Unable to open %a for writing (%s). No report generated"
+ Filepath.Normalized.pretty file s
diff --git a/src/plugins/markdown-report/mdr_params.ml b/src/plugins/markdown-report/mdr_params.ml
index 3b799faccaad2e5e4349c5ebe73993683abf2dbb..12d8cfbf603b1ea4f869c8aa011538b5f254462c 100644
--- a/src/plugins/markdown-report/mdr_params.ml
+++ b/src/plugins/markdown-report/mdr_params.ml
@@ -39,33 +39,36 @@ module Generate = String(
none (default), md, draft and sarif"
end)
-module Output : Parameter_sig.String =
+module Output : Parameter_sig.Filepath =
struct
- include String(
+ include Filepath(
struct
let option_name = "-mdr-out"
let arg_name = "f"
- let default = "report"
+ let file_kind = "Report"
+ let existence = Fc_Filepath.Indifferent
let help = "sets the name of the output file to <f>. \
If <f> has no extension, it is chosen automatically based on \
the report kind"
end)
let get () =
let s = get () in
- if Pervasives_string.contains (Filename.basename s) '.' then s
+ if Pervasives_string.contains (Filename.basename (s:>string)) '.' then s
else
let kind = Generate.get () in
let ext = if kind = "sarif" then ".sarif" else ".md" in
- s ^ ext
+ Fc_Filepath.Normalized.concat s ext
end
let () =
Generate.set_possible_values [ "none"; "md"; "draft"; "sarif" ]
-module Remarks = Empty_string(
+module Remarks = Filepath(
struct
let option_name = "-mdr-remarks"
let arg_name = "f"
+ let file_kind = "Remarks file"
+ let existence = Fc_Filepath.Must_exist
let help =
"reads file <f> to add additional remarks to various sections of the report. \
Must be in a format compatible with the file produced by -mdr-gen-draft. \
diff --git a/src/plugins/markdown-report/mdr_params.mli b/src/plugins/markdown-report/mdr_params.mli
index b7c5b06901b78d086f8389fa5fe8adf149d07112..f40ba97f1b52665c59872985be6bfd728725fa80 100644
--- a/src/plugins/markdown-report/mdr_params.mli
+++ b/src/plugins/markdown-report/mdr_params.mli
@@ -23,13 +23,13 @@
include Plugin.S
(** Value of [-mdr-out]. *)
-module Output: Parameter_sig.String
+module Output: Parameter_sig.Filepath
(** Value of [-mdr-gen]. *)
module Generate: Parameter_sig.String
(** Value of [-mdr-remarks]. *)
-module Remarks: Parameter_sig.String
+module Remarks: Parameter_sig.Filepath
(** Value of [-mdr-flamegraph]. *)
module FlameGraph: Parameter_sig.String
diff --git a/src/plugins/markdown-report/parse_remarks.ml b/src/plugins/markdown-report/parse_remarks.ml
index d2e4860e7c455fb1f4fc6b477c3882b2ffc653da..10fc83a0da5af95687e7ec085acff31c9de2337e 100644
--- a/src/plugins/markdown-report/parse_remarks.ml
+++ b/src/plugins/markdown-report/parse_remarks.ml
@@ -112,13 +112,15 @@ let parse_remarks env chan =
env
let get_remarks f =
- Mdr_params.debug ~dkey "Using remarks file %s" f;
+ Mdr_params.debug ~dkey "Using remarks file %a"
+ Filepath.Normalized.pretty f;
try
- let chan = open_in f in
+ let chan = open_in (f:>string) in
let { remarks } = parse_remarks (empty_env ()) chan in
remarks
with Sys_error err ->
Mdr_params.error
- "Unable to open remarks file %s (%s). \
- No additional remarks will be included in the report." f err;
+ "Unable to open remarks file %a (%s). \
+ No additional remarks will be included in the report."
+ Filepath.Normalized.pretty f err;
Datatype.String.Map.empty
diff --git a/src/plugins/markdown-report/parse_remarks.mli b/src/plugins/markdown-report/parse_remarks.mli
index 2491fe94a4998fe29fed358596b97815f98da233..48728e02729fbad4a37dc3647d8153d729cfdc69 100644
--- a/src/plugins/markdown-report/parse_remarks.mli
+++ b/src/plugins/markdown-report/parse_remarks.mli
@@ -25,4 +25,4 @@
(** [get_remarks f] retrieves the elements associated to various sections
of the report, referenced by their anchor. *)
-val get_remarks: string -> Markdown.element list Datatype.String.Map.t
+val get_remarks: Filepath.Normalized.t -> Markdown.element list Datatype.String.Map.t
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 12d64ad6e94bf30041c359bf8bb4d705e75a29f7..62ee563dbe9f07043c858439d9daab6353bd2304 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -38,8 +38,8 @@ let frama_c_sarif () =
~informationUri ())
let get_remarks () =
- let f = Mdr_params.Remarks.get () in
- if f <> "" then Parse_remarks.get_remarks f
+ if not (Mdr_params.Remarks.is_empty ()) then
+ Parse_remarks.get_remarks (Mdr_params.Remarks.get ())
else Datatype.String.Map.empty
let get_remark remarks label =
@@ -273,13 +273,14 @@ let generate () =
let remarks = get_remarks () in
let runs = [ gen_run remarks ] in
let json = Schema.create ~runs () |> Schema.to_yojson in
- let file = Mdr_params.Output.get () in
- if file = "" then
- Log.print_on_output (fun fmt -> Yojson.Safe.pretty_print fmt json)
- else
+ if not (Mdr_params.Output.is_empty ()) then
+ let file = Mdr_params.Output.get () in
try
- Command.write_file file
+ Command.write_file (file:>string)
(fun out -> Yojson.Safe.pretty_to_channel ~std:true out json) ;
- Mdr_params.result "Report %s generated" file
+ Mdr_params.result "Report %a generated" Filepath.Normalized.pretty file
with Sys_error s ->
- Mdr_params.abort "Unable to generate %s (%s)" file s
+ Mdr_params.abort "Unable to generate %a (%s)"
+ Filepath.Normalized.pretty file s
+ else
+ Log.print_on_output (fun fmt -> Yojson.Safe.pretty_print fmt json)
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index 75acb89eb4d1ed53cd438c23c2e0af51e3e6fcd8..9800d450ab5c59d5bb1a1c992edcd52403c8d4b6 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -308,10 +308,10 @@ let dump_acsl_stats_html fmt =
let dump () =
- let out = Metrics_parameters.OutputFile.get () in
- if out <> "" then begin
+ if not (Metrics_parameters.OutputFile.is_empty ()) then begin
+ let out = Metrics_parameters.OutputFile.get () in
try
- let chan = open_out out in
+ let chan = open_out (out:>string) in
let fmt = Format.formatter_of_out_channel chan in
(match Metrics_base.get_file_type out with
| Metrics_base.Html -> dump_acsl_stats_html fmt
@@ -322,6 +322,7 @@ let dump () =
);
close_out chan
with Sys_error s ->
- Metrics_parameters.abort "Cannot open file %s (%s)" out s
+ Metrics_parameters.abort "Cannot open file %a (%s)"
+ Filepath.Normalized.pretty out s
end else Metrics_parameters.result "%t" dump_acsl_stats
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index a29fdada1c39483d090761c6af07185d31df7d24..4555837a8811f08bce4a738427e8625889174f41 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -251,9 +251,9 @@ type output_type =
| Json
;;
-let get_file_type filename =
+let get_file_type (filename : Filepath.Normalized.t) =
try
- match get_suffix filename with
+ match get_suffix (filename:>string) with
| "html" | "htm" -> Html
| "txt" | "text" -> Text
| "json" -> Json
@@ -263,7 +263,8 @@ let get_file_type filename =
with
| No_suffix ->
Metrics_parameters.abort
- "File %s has no suffix. Cannot produce output.@." filename
+ "File %a has no suffix. Cannot produce output.@."
+ Filepath.Normalized.pretty filename
module VarinfoByName = struct
type t = Cil_types.varinfo
diff --git a/src/plugins/metrics/metrics_base.mli b/src/plugins/metrics/metrics_base.mli
index f4c84845ca1c4ca177dd1c2fbd555e0cec255d88..a93c078c04ecda52d352be849d92e39e9da8174a 100644
--- a/src/plugins/metrics/metrics_base.mli
+++ b/src/plugins/metrics/metrics_base.mli
@@ -146,7 +146,7 @@ type output_type =
(** get_file_type [extension] sets the output type according to [extension].
Raises an error if [extension] is not among supported extensions or is empty.
*)
-val get_file_type: string -> output_type;;
+val get_file_type: Filepath.Normalized.t -> output_type;;
(** consider_function [vinfo] returns false if the varinfo is not a function we
are interested in.
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 962ed38461e91ff9f4f4e810d6cd14f4b026b7bb..5abd0b83e04bf242ddf98095cc3dcf365be1f7f2 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -734,25 +734,25 @@ let compute_on_cilast ~libc =
"@[<v 0>Cil AST@ %t@]" cil_visitor#pp_detailed_text_metrics;
(* let r = metrics_to_result cil_visitor in *)
(* Print the result to file if required *)
- let out_fname = Metrics_parameters.OutputFile.get () in
- begin
- if out_fname <> "" then
- try
- let oc = open_out_bin out_fname in
- let fmt = Format.formatter_of_out_channel oc in
- (match Metrics_base.get_file_type out_fname with
- | Html -> dump_html fmt cil_visitor
- | Text -> pp_with_funinfo fmt cil_visitor
- | Json ->
- let json = json_of_funinfo cil_visitor in
- Yojson.pretty_print fmt json;
- Format.fprintf fmt "@." (* ensure the file ends with a newline *)
- );
- close_out oc;
- with Sys_error _ ->
- Metrics_parameters.failure "Cannot open file %s.@." out_fname
- else Metrics_parameters.result "%a" pp_with_funinfo cil_visitor
+ if not (Metrics_parameters.OutputFile.is_empty ()) then begin
+ let out_fname = Metrics_parameters.OutputFile.get () in
+ try
+ let oc = open_out_bin (out_fname:>string) in
+ let fmt = Format.formatter_of_out_channel oc in
+ (match Metrics_base.get_file_type out_fname with
+ | Html -> dump_html fmt cil_visitor
+ | Text -> pp_with_funinfo fmt cil_visitor
+ | Json ->
+ let json = json_of_funinfo cil_visitor in
+ Yojson.pretty_print fmt json;
+ Format.fprintf fmt "@." (* ensure the file ends with a newline *)
+ );
+ close_out oc;
+ with Sys_error _ ->
+ Metrics_parameters.failure "Cannot open file %a.@."
+ Filepath.Normalized.pretty out_fname
end
+ else Metrics_parameters.result "%a" pp_with_funinfo cil_visitor
(* Visitor for the recursive estimation of a stack size.
Its arguments are the function currently being visited and the current
diff --git a/src/plugins/metrics/metrics_parameters.ml b/src/plugins/metrics/metrics_parameters.ml
index 30ae2ef4d389e1a3db3a9e0f5e8fe3e35c7ac1bd..5aeae5dc6886cb3b151c7a285471a7421f72e207 100644
--- a/src/plugins/metrics/metrics_parameters.ml
+++ b/src/plugins/metrics/metrics_parameters.ml
@@ -44,10 +44,12 @@ module ByFunction =
end)
module OutputFile =
- Empty_string
+ Filepath
(struct
let option_name = "-metrics-output"
let arg_name = "filename"
+ let file_kind = "Text, HTML or JSON"
+ let existence = Fc_Filepath.Indifferent
let help = "print some metrics into the specified file; \
the output format is recognized through the extension: \
.text/.txt for text, .html/.htm for HTML, or .json for JSON."
diff --git a/src/plugins/metrics/metrics_parameters.mli b/src/plugins/metrics/metrics_parameters.mli
index bc9a5e556236fb042b721a5f4bed701c44b00db8..990c31c6751adcd6cd7eced29131fc2f796fb0ae 100644
--- a/src/plugins/metrics/metrics_parameters.mli
+++ b/src/plugins/metrics/metrics_parameters.mli
@@ -35,7 +35,7 @@ module ValueCoverage: Parameter_sig.With_output
module AstType: Parameter_sig.String
(** Set the ASTs on which the metrics should be computed *)
-module OutputFile: Parameter_sig.String
+module OutputFile: Parameter_sig.Filepath
(** Pretty print metrics to the given file.
The output format will be recognized through the extension.
Supported extensions are:
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 1c6c22f3d644838f5ab6dbbe6e833784f446642e..eab82120d48a99be2b60ec2b7575f82e4fb2f4fa 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -520,14 +520,14 @@ let report_dump fmt =
end
let report_output file =
- R.feedback "Output %s@." file ;
- Command.print_file file report_dump
+ R.feedback "Output %a@." Filepath.Normalized.pretty file;
+ Command.print_file (file:>string) report_dump
let report_number name nb opt =
if nb > 0 then R.feedback "%s%4d" name nb ;
let file = opt () in
- if file <> "" then
- let out = open_out file in
+ if not (Filepath.Normalized.is_empty file) then
+ let out = open_out (file:>string) in
output_string out (string_of_int nb) ;
flush out ; close_out out
@@ -540,8 +540,7 @@ let classify () =
(not (R.Stderr.get ()) &&
not (R.Output.is_set ()))
then report_console () ;
- let file = R.Output.get () in
- if file <> "" then report_output file ;
+ if not (R.Output.is_empty ()) then report_output (R.Output.get ());
report_number "Reviews : " !nb_reviews R.OutputReviews.get ;
report_number "Errors : " !nb_errors R.OutputErrors.get ;
report_number "Unclassified: " !nb_unclassified R.OutputUnclassified.get ;
diff --git a/src/plugins/report/csv.ml b/src/plugins/report/csv.ml
index bd6becb61a8ef9dbb6b4dde3387827fcfec7fa71..b4120daeb835084b1bb6c905e8390731424bbec9 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -95,8 +95,9 @@ let print_csv =
let print_csv_once () =
let file = Report_parameters.CSVFile.get () in
- Report_parameters.feedback "Dumping properties in '%s'" file;
- print_csv file
+ Report_parameters.feedback "Dumping properties in '%a'"
+ Filepath.Normalized.pretty file;
+ print_csv (file:>string)
let print_csv, _ =
State_builder.apply_once
@@ -107,7 +108,8 @@ let print_csv, _ =
Property_status.self ]
print_csv_once
-let main () = if Report_parameters.CSVFile.get () <> "" then print_csv ()
+let main () =
+ if not (Report_parameters.CSVFile.is_empty ()) then print_csv ()
let () = Db.Main.extend main
diff --git a/src/plugins/report/report_parameters.ml b/src/plugins/report/report_parameters.ml
index b7f24343af6f4afc0dc5e609f2d6e535c0e3e42a..da18d1ca076be5d29c04d093f6f9ca169dfc57e4 100644
--- a/src/plugins/report/report_parameters.ml
+++ b/src/plugins/report/report_parameters.ml
@@ -73,11 +73,12 @@ module Proven =
let () = Parameter_customize.set_group printing
module CSVFile =
- String
+ Filepath
(struct
let option_name = "-report-csv"
let arg_name = "name"
- let default = ""
+ let file_kind = "CSV"
+ let existence = Fc_Filepath.Indifferent
let help = "if set, output properties as a csv file of the given name"
end)
@@ -166,12 +167,13 @@ module InvalidStatus =
let () = Parameter_customize.set_group monitoring
module Output =
- String
+ Filepath
(struct
let option_name = "-report-output"
let arg_name = "*.json"
+ let file_kind = "JSON"
+ let existence = Fc_Filepath.Indifferent
let help = "Output -report-classify in JSON format"
- let default = ""
end)
let () = Parameter_customize.set_group monitoring
@@ -184,32 +186,35 @@ module AbsolutePath =
let () = Parameter_customize.set_group monitoring
module OutputReviews =
- String
+ Filepath
(struct
let option_name = "-report-output-reviews"
let arg_name = "file"
+ let file_kind = "Text"
+ let existence = Fc_Filepath.Indifferent
let help = "Output number of reviews to <file>"
- let default = ""
end)
let () = Parameter_customize.set_group monitoring
module OutputErrors =
- String
+ Filepath
(struct
let option_name = "-report-output-errors"
let arg_name = "file"
+ let file_kind = "Text"
+ let existence = Fc_Filepath.Indifferent
let help = "Output number of errors to <file>"
- let default = ""
end)
let () = Parameter_customize.set_group monitoring
module OutputUnclassified =
- String
+ Filepath
(struct
let option_name = "-report-output-unclassified"
let arg_name = "file"
+ let file_kind = "Text"
+ let existence = Fc_Filepath.Indifferent
let help = "Output number of unclassified to <file>"
- let default = ""
end)
let () = Parameter_customize.set_group monitoring
diff --git a/src/plugins/report/report_parameters.mli b/src/plugins/report/report_parameters.mli
index 0f806eeed28e8f2741737097c5079fa667404ac9..80602986b49cf3ff4669859c0bc49a1e9fa1ae84 100644
--- a/src/plugins/report/report_parameters.mli
+++ b/src/plugins/report/report_parameters.mli
@@ -29,7 +29,7 @@ module Untried: Parameter_sig.Bool
module Specialized: Parameter_sig.Bool
module Proven: Parameter_sig.Bool
-module CSVFile: Parameter_sig.String
+module CSVFile: Parameter_sig.Filepath
module Classify: Parameter_sig.Bool
module Rules: Parameter_sig.String_list
module Warning: Parameter_sig.String
@@ -39,10 +39,10 @@ module UntriedStatus: Parameter_sig.String
module UnknownStatus: Parameter_sig.String
module InvalidStatus: Parameter_sig.String
-module Output: Parameter_sig.String
-module OutputReviews: Parameter_sig.String
-module OutputErrors: Parameter_sig.String
-module OutputUnclassified: Parameter_sig.String
+module Output: Parameter_sig.Filepath
+module OutputReviews: Parameter_sig.Filepath
+module OutputErrors: Parameter_sig.Filepath
+module OutputUnclassified: Parameter_sig.Filepath
module AbsolutePath: Parameter_sig.Bool
module Stdout: Parameter_sig.Bool
module Stderr: Parameter_sig.Bool
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index f38f08705f929dc2d66c7b02a8acd4678acee133..206ebd4ca538956d506237e164f49b170773b16e 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -307,16 +307,17 @@ let metadata page : json =
(* -------------------------------------------------------------------------- *)
let pp_one_page ~root ~page ~title body =
- let full_path = Filepath.normalize (root ^ "/" ^ page) in
- let dir = Filename.dirname full_path in
+ let full_path = Filepath.Normalized.concat root page in
+ let dir = Filename.dirname (full_path:>string) in
if not (Sys.file_exists dir) then Extlib.mkdir ~parents:true dir 0o755;
try
- let chan = open_out full_path in
+ let chan = open_out (full_path:>string) in
let fmt = Format.formatter_of_out_channel chan in
let title = Md.plain title in
Markdown.(pp_pandoc ~page fmt (pandoc ~title body))
with Sys_error e ->
- Senv.fatal "Could not open file %s for writing: %s" full_path e
+ Senv.fatal "Could not open file %a for writing: %s"
+ Filepath.Normalized.pretty full_path e
(* Build section contents in reverse order *)
let build d s = List.fold_left (fun d s -> s() :: d) d s
@@ -338,13 +339,13 @@ let dump ~root ?(meta=true) () =
let body = Markdown.subsections page.descr (build [] page.sections) in
pp_one_page ~root ~page:path ~title (intro @ body) ;
if meta then
- let path = Printf.sprintf "%s/%s.json" root path in
- Yojson.Basic.to_file path (metadata page) ;
+ let path = Filepath.Normalized.concat root (path ^ ".json") in
+ Yojson.Basic.to_file (path:>string) (metadata page) ;
) !pages ;
Senv.feedback "[doc] Page: 'readme.md'" ;
if meta then
- let path = Printf.sprintf "%s/readme.md.json" root in
- Yojson.Basic.to_file path maindata ;
+ let path = Filepath.Normalized.concat root "readme.md.json" in
+ Yojson.Basic.to_file (path:>string) maindata ;
let body =
[ Md.H1 (Md.plain "Presentation", None);
Md.Block (Md.text (Md.format "Version %s" Fc_config.version))]
@@ -362,16 +363,17 @@ let dump ~root ?(meta=true) () =
let () =
Db.Main.extend begin
fun () ->
- let root = Senv.Doc.get () in
- if root <> "" then
- if Sys.file_exists root && Sys.is_directory root then
+ if not (Senv.Doc.is_empty ()) then
+ let root = Senv.Doc.get () in
+ if Sys.is_directory (root:>string) then
begin
- Senv.feedback "[doc] Root: '%s'" root ;
+ Senv.feedback "[doc] Root: '%a'" Filepath.Normalized.pretty root ;
Package.iter package ;
dump ~root () ;
end
else
- Senv.error "[doc] File '%s' is not a directory" root
+ Senv.error "[doc] File '%a' is not a directory"
+ Filepath.Normalized.pretty root
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_doc.mli b/src/plugins/server/server_doc.mli
index 6bb0462554ea7348d1133a53bd925ed4f62098ab..d86aaa97d5be52ac58a8cbb44ce264eb18c52ae8 100644
--- a/src/plugins/server/server_doc.mli
+++ b/src/plugins/server/server_doc.mli
@@ -72,6 +72,6 @@ val package : Package.packageInfo -> unit
(** Dumps all published pages of documentations. Unless [~meta:false], also
generates METADATA for each page in [<filename>.json] for each page. *)
-val dump : root:string -> ?meta:bool -> unit -> unit
+val dump : root:Filepath.Normalized.t -> ?meta:bool -> unit -> unit
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index 3eedff1c7280142bea5b0bdd536b36eb50a384d6..c7086902c978644aa8f1d127c3bc115d0d378654 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -60,11 +60,12 @@ let server_doc = add_group "Server Doc Generation"
let () = Parameter_customize.set_group server_doc
let () = Parameter_customize.do_not_save ()
-module Doc = P.String
+module Doc = P.Filepath
(struct
let option_name = "-server-doc"
let arg_name = "dir"
- let default = ""
+ let file_kind = "Directory"
+ let existence = Fc_Filepath.Must_exist
let help = "Output a markdown documentation of the server in <dir>"
end)
diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli
index 4186a397421ee6135487e34a06ad7b1bc90b3f13..74d29a8d0c1a1575ff25bbb0906f97b80905516d 100644
--- a/src/plugins/server/server_parameters.mli
+++ b/src/plugins/server/server_parameters.mli
@@ -24,7 +24,7 @@
include Plugin.General_services
-module Doc : Parameter_sig.String (** Generate documentation *)
+module Doc : Parameter_sig.Filepath (** Generate documentation *)
module Polling : Parameter_sig.Int (** Idle waiting time (in ms) *)
module AutoLog : Parameter_sig.Bool (** Monitor logs *)
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index cafa9a5f1da9f06c0be6fedbffbec0f6e4117543..e2afa36684c692128b90b61eed91623cce461df9 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -86,14 +86,14 @@ module Domain = struct
include Simple_memory.Make_Domain (Name) (Numerors_Value)
let post_analysis f =
- match f, Value_parameters.NumerorsLogFile.get () with
- | _, s when s = "" -> ()
- | `Value _, s ->
- let log = open_out s in
- let fmt = Format.formatter_of_out_channel log in
- List.iter (fun f -> f fmt ()) !Numerors_Value.dprint_callstack ;
- close_out log
- | _, _ -> ()
+ if not (Value_parameters.NumerorsLogFile.is_empty ()) then
+ match f with
+ | `Value _ ->
+ let log = open_out (Value_parameters.NumerorsLogFile.get ():>string) in
+ let fmt = Format.formatter_of_out_channel log in
+ List.iter (fun f -> f fmt ()) !Numerors_Value.dprint_callstack ;
+ close_out log
+ | _ -> ()
end
(* Reduced product between the cvalue values and the numerors values. *)
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index ce718b03ee17ad5b2c30afd9a4d08658f3b5f7ee..408114d15682d5121126bb154111f216bf67c8f6 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -1278,7 +1278,7 @@ module D = struct
Value_parameters.failure "The trace is TOP can't generate code"
| `Value state ->
if not (Value_parameters.TracesDot.is_default ())
- then output_dot (Value_parameters.TracesDot.get ()) state;
+ then output_dot (Value_parameters.TracesDot.get ():>string) state;
if Value_parameters.TracesProject.get ()
then project_of_cfg return_exp state
end
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 93fd504680369faf45e68100017c4acf5552ea39..33c7c3687c564d51e19b87ceca850b0687a751a2 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -173,10 +173,10 @@ let reset_analyzer () =
let force_compute () =
Ast.compute ();
Value_parameters.configure_precision ();
- if not (Filepath.Normalized.is_unknown (Kernel.AuditCheck.get ()))
- then Eva_audit.check_configuration (Kernel.AuditCheck.get ());
- if not (Filepath.Normalized.is_unknown (Kernel.AuditPrepare.get ()))
- then Eva_audit.print_configuration (Kernel.AuditPrepare.get ());
+ if not (Kernel.AuditCheck.is_empty ()) then
+ Eva_audit.check_configuration (Kernel.AuditCheck.get ());
+ if not (Kernel.AuditPrepare.is_empty ()) then
+ Eva_audit.print_configuration (Kernel.AuditPrepare.get ());
let kf, lib_entry = Globals.entry_point () in
reset_analyzer ();
let module Analyzer = (val snd !ref_analyzer) in
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index 8657a9dae7c99b77cd9bb5e7c11f0b9d33a708bb..cd194c77d7a2ef18a4cc3bb67e224939e2e56e04 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -175,8 +175,9 @@ let print_information fmt { loc; kf; alarm; kind; text; status; contexts } =
dir file lnum kf alarm kind contexts status text
let output file =
- Value_parameters.feedback "Listing red statuses in file %s" file;
- let channel = open_out file in
+ Value_parameters.feedback "Listing red statuses in file %a"
+ Filepath.Normalized.pretty file;
+ let channel = open_out (file:>string) in
let fmt = Format.formatter_of_out_channel channel in
Format.pp_set_margin fmt 1000000;
Format.fprintf fmt "@[<v>";
@@ -189,5 +190,4 @@ let output file =
Format.fprintf fmt "@]%!"
let report () =
- let file = Value_parameters.ReportRedStatuses.get () in
- if file <> "" then output file
+ Value_parameters.ReportRedStatuses.(if not (is_empty ()) then output (get ()))
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index e8f0be51619f58a5a7003874680638b01b43d8a4..b4c455f6db589faaba2a24fbf63646b29526febf 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -395,11 +395,11 @@ let start_doing_flamegraph callstack =
| [] -> assert false
| [_] ->
(* Analysis of main *)
- let file = Value_parameters.ValPerfFlamegraphs.get () in
- if file <> "" then begin
+ if not (Value_parameters.ValPerfFlamegraphs.is_empty ()) then begin
+ let file = Value_parameters.ValPerfFlamegraphs.get () in
try
(* Flamegraphs must be computed. Set up the stack and the output file *)
- let oc = open_out file in
+ let oc = open_out (file:>string) in
oc_flamegraph := Some oc;
stack_flamegraph := [ (Sys.time (), 0.) ]
with e ->
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index ec4e77fd3ed01fec6b323a0129a6a1f580db8bd0..494a55fc98f21b9986e5d52116d7f3aacecf67aa 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -351,11 +351,13 @@ module TracesUnifyLoop =
let () = add_precision_dep TracesUnifyLoop.parameter
let () = Parameter_customize.set_group domains
-module TracesDot = Empty_string
+module TracesDot = Filepath
(struct
let option_name = "-eva-traces-dot"
- let help = "Output to the given filename the Cfg in dot format."
let arg_name = "FILENAME"
+ let file_kind = "DOT"
+ let existence = Fc_Filepath.Indifferent
+ let help = "Output to the given filename the Cfg in dot format."
end)
let () = Parameter_customize.set_group domains
@@ -1070,14 +1072,15 @@ module ValShowPerf =
let () = Parameter_customize.set_group messages
module ValPerfFlamegraphs =
- String
+ Filepath
(struct
let option_name = "-eva-flamegraph"
+ let arg_name = "file"
+ let file_kind = "Text for flamegraph"
+ let existence = Fc_Filepath.Indifferent
let help = "Dump a summary of the time spent analyzing function calls \
in a format suitable for the Flamegraph tool \
(http://www.brendangregg.com/flamegraphs.html)"
- let arg_name = "file"
- let default = ""
end)
@@ -1103,11 +1106,12 @@ module PrintCallstacks =
let () = Parameter_customize.set_group messages
module ReportRedStatuses =
- String
+ Filepath
(struct
let option_name = "-eva-report-red-statuses"
let arg_name = "filename"
- let default = ""
+ let file_kind = "CSV"
+ let existence = Fc_Filepath.Indifferent
let help = "Output the list of \"red properties\" in a csv file of the \
given name. These are the properties which were invalid for \
some states. Their consolidated status may not be invalid, \
@@ -1116,13 +1120,14 @@ module ReportRedStatuses =
let () = Parameter_customize.set_group messages
module NumerorsLogFile =
- String
+ Filepath
(struct
let option_name = "-eva-numerors-log-file"
+ let arg_name = "file"
+ let file_kind = "Text"
+ let existence = Fc_Filepath.Indifferent
let help = "The Numerors domain will save each call to the DPRINT \
function in the given file"
- let arg_name = "file"
- let default = ""
end)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 3f50d6efaa7990c3c68289b0043e4259bab34ba0..9a6a7172cc20cf89b2a178a6bf40c59cf1e91779 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -42,7 +42,7 @@ module OctagonCall: Parameter_sig.Bool
module TracesUnrollLoop: Parameter_sig.Bool
module TracesUnifyLoop: Parameter_sig.Bool
-module TracesDot: Parameter_sig.String
+module TracesDot: Parameter_sig.Filepath
module TracesProject: Parameter_sig.Bool
module EqualityStorage: Parameter_sig.Bool
@@ -122,11 +122,11 @@ module SplitGlobalStrategy: State_builder.Ref with type data = Split_strategy.t
module ValShowProgress: Parameter_sig.Bool
module ValShowPerf: Parameter_sig.Bool
-module ValPerfFlamegraphs: Parameter_sig.String
+module ValPerfFlamegraphs: Parameter_sig.Filepath
module ShowSlevel: Parameter_sig.Int
module PrintCallstacks: Parameter_sig.Bool
-module ReportRedStatuses: Parameter_sig.String
-module NumerorsLogFile: Parameter_sig.String
+module ReportRedStatuses: Parameter_sig.Filepath
+module NumerorsLogFile: Parameter_sig.Filepath
module MemExecAll: Parameter_sig.Bool
diff --git a/tests/crowbar/test_ghost_cfg.ml b/tests/crowbar/test_ghost_cfg.ml
index cc91a8af05d2d6259b9edb867296fe76f2cd96e9..5f67349aee7aec87e003b56d33b1dac317de6964 100644
--- a/tests/crowbar/test_ghost_cfg.ml
+++ b/tests/crowbar/test_ghost_cfg.ml
@@ -460,7 +460,7 @@ let gen_file =
f.svar.vdefined <- true;
f.sbody <- body;
(env,
- { fileName = Filepath.Normalized.unknown;
+ { fileName = Filepath.Normalized.empty;
globals = [
GVarDecl (x,Cil_datatype.Location.unknown);
GVarDecl (y,Cil_datatype.Location.unknown);