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 778c405744373a9968683061f1beb012c2fc3453..e0edf8abfab073a2744df8bb1db580eae191c358 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -87,7 +87,7 @@ let () =
(* Load Frama-c from disk if required *)
let load_binary () =
- if Kernel.LoadState.is_known () then begin
+ if not (Kernel.LoadState.is_empty ()) then begin
let filepath = Kernel.LoadState.get () in
try
Project.load_all filepath
@@ -133,7 +133,7 @@ let () = Extlib.safe_at_exit time
(* Save Frama-c on disk if required *)
let save_binary error_extension =
- if Kernel.SaveState.is_known () then begin
+ if not (Kernel.SaveState.is_empty ()) then begin
let filename = Kernel.SaveState.get () in
Kernel.SaveState.clear ();
let realname =
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 0f17bfc1a580fcbcbab542268db8500447d33996..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 Kernel.JsonCompilationDatabase.is_known () 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 20b9317afa9f7cd1a30781be18c047ebfedeeebb..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,7 +532,7 @@ struct
else
p
- let is_known () = not (Filepath.Normalized.is_unknown (get ()))
+ 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 b4025f9c382ced0f0df597f4fd8a7ce449eb538a..4d16f3101e799b36e4bad457557a6fbf44c31db1 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -297,11 +297,11 @@ module type Filepath = sig
include S with type t = Filepath.Normalized.t
(**
- Whether the Filepath is known, e.g. not empty.
+ Whether the Filepath is empty.
@since Frama-C+dev
*)
- val is_known: unit -> bool
+ val is_empty: unit -> bool
end
(** signature for searching files in a specific directory. *)
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 9864027d2d1f48c4e6e781d67d281b0e841a824f..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 Buchi.is_known () then Buchi.get () else To_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 1b47e26b755ee63198546c9602c8978606b02fd6..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 not (Aorai_option.Ya.is_known ()) then
- if not (Aorai_option.Buchi.is_known ()) 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 Aorai_option.To_Buchi.is_known () 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,7 +203,7 @@ let init_file_names () =
Extlib.cleanup_at_exit (!promela_file :> string);
end
end else begin
- if Aorai_option.To_Buchi.is_known () && Aorai_option.Ltl_File.is_known ()
+ 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' \
@@ -216,7 +216,7 @@ let init_file_names () =
dot_file := freshname !promela_file ".dot";
end
else begin
- if not (Aorai_option.Ya.is_known ()) then
+ if Aorai_option.Ya.is_empty () then
Aorai_option.abort "empty Ya file name";
if Aorai_option.Dot.get() then
dot_file := freshname (Aorai_option.Ya.get ()) ".dot"
@@ -240,8 +240,8 @@ let work () =
let file = Ast.get () in
Aorai_utils.initFile file;
printverb "C file loading : done\n";
- if not (Aorai_option.Ya.is_known ()) then
- if not (Aorai_option.Buchi.is_known ()) 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"
@@ -252,16 +252,16 @@ let work () =
Aorai_option.abort "failed to run: %s" cmd ;
printverb "LTL ~> Promela (ltl2ba): done\n"
end;
- if Aorai_option.To_Buchi.is_known () 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 Aorai_option.Buchi.is_known () then
+ if not (Aorai_option.Buchi.is_empty ()) then
load_promela_file_withexps !promela_file
- else if Aorai_option.Ya.is_known () 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/register.ml b/src/plugins/callgraph/register.ml
index dbe891b5ad6b4f042711406d97114538ec95c06f..487f6d51055e43009da0df956a6e071653fd135d 100644
--- a/src/plugins/callgraph/register.ml
+++ b/src/plugins/callgraph/register.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
let main () =
- if Options.Filename.is_known () 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 c90fcad5e55253035952c10f1de9cfb68fdb7201..10d3da3b178ed82ae91cff195a264c333b5072ef 100644
--- a/src/plugins/dive/main.ml
+++ b/src/plugins/dive/main.ml
@@ -57,9 +57,9 @@ let main () =
if not (Self.FromFunctionAlarms.is_empty ()) then
Alarms.iter add_alarm;
(* Output it *)
- if Self.OutputDot.is_known () then
+ if not (Self.OutputDot.is_empty ()) then
output Dot context (Self.OutputDot.get ());
- if Self.OutputJson.is_known () then
+ if not (Self.OutputJson.is_empty ()) then
output Json context (Self.OutputJson.get ());
end
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index c3e8c3291c66bf20ec16f544675f61f556d5b062..b8a09ed3b99df3c6f9b02ba4b5bb1b5bb427c4a4 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -554,7 +554,7 @@ let gen_alarms env =
gen_section_postlude env
let mk_remarks is_draft =
- if Mdr_params.Remarks.is_known () then
+ 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
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 4c604024a7759736e9f8cbca0ad83804c9782c5e..62ee563dbe9f07043c858439d9daab6353bd2304 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -38,7 +38,7 @@ let frama_c_sarif () =
~informationUri ())
let get_remarks () =
- if Mdr_params.Remarks.is_known () then
+ if not (Mdr_params.Remarks.is_empty ()) then
Parse_remarks.get_remarks (Mdr_params.Remarks.get ())
else Datatype.String.Map.empty
@@ -273,7 +273,7 @@ let generate () =
let remarks = get_remarks () in
let runs = [ gen_run remarks ] in
let json = Schema.create ~runs () |> Schema.to_yojson in
- if Mdr_params.Output.is_known () then
+ if not (Mdr_params.Output.is_empty ()) then
let file = Mdr_params.Output.get () in
try
Command.write_file (file:>string)
diff --git a/src/plugins/metrics/metrics_acsl.ml b/src/plugins/metrics/metrics_acsl.ml
index 23a82ce104e4cf21b89d927b0b2653ae18d713a4..9800d450ab5c59d5bb1a1c992edcd52403c8d4b6 100644
--- a/src/plugins/metrics/metrics_acsl.ml
+++ b/src/plugins/metrics/metrics_acsl.ml
@@ -308,7 +308,7 @@ let dump_acsl_stats_html fmt =
let dump () =
- if Metrics_parameters.OutputFile.is_known () then begin
+ if not (Metrics_parameters.OutputFile.is_empty ()) then begin
let out = Metrics_parameters.OutputFile.get () in
try
let chan = open_out (out:>string) in
diff --git a/src/plugins/metrics/metrics_cilast.ml b/src/plugins/metrics/metrics_cilast.ml
index 27dd410c567b55472231cafd224c4f2e90b28009..5abd0b83e04bf242ddf98095cc3dcf365be1f7f2 100644
--- a/src/plugins/metrics/metrics_cilast.ml
+++ b/src/plugins/metrics/metrics_cilast.ml
@@ -734,7 +734,7 @@ 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 *)
- if Metrics_parameters.OutputFile.is_known () then begin
+ 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
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 51bad186a8e0df32b86dc6f65783f337439c0cc0..eab82120d48a99be2b60ec2b7575f82e4fb2f4fa 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -526,7 +526,7 @@ let report_output file =
let report_number name nb opt =
if nb > 0 then R.feedback "%s%4d" name nb ;
let file = opt () in
- if not (Filepath.Normalized.is_unknown file) then
+ 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,7 +540,7 @@ let classify () =
(not (R.Stderr.get ()) &&
not (R.Output.is_set ()))
then report_console () ;
- if R.Output.is_known () then report_output (R.Output.get ());
+ 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 8b91a930bd67e479de922b716310fe353501f431..b4120daeb835084b1bb6c905e8390731424bbec9 100644
--- a/src/plugins/report/csv.ml
+++ b/src/plugins/report/csv.ml
@@ -109,7 +109,7 @@ let print_csv, _ =
print_csv_once
let main () =
- if Report_parameters.CSVFile.is_known () then print_csv ()
+ if not (Report_parameters.CSVFile.is_empty ()) then print_csv ()
let () = Db.Main.extend main
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 813042ddbad6d87ba8a3ba0914a0c2e69bc2b4dd..206ebd4ca538956d506237e164f49b170773b16e 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -363,7 +363,7 @@ let dump ~root ?(meta=true) () =
let () =
Db.Main.extend begin
fun () ->
- if Senv.Doc.is_known () then
+ if not (Senv.Doc.is_empty ()) then
let root = Senv.Doc.get () in
if Sys.is_directory (root:>string) then
begin
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index d765cef07fafe7ae04f6d57ff2ce0c55aba69799..e2afa36684c692128b90b61eed91623cce461df9 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -86,7 +86,7 @@ module Domain = struct
include Simple_memory.Make_Domain (Name) (Numerors_Value)
let post_analysis f =
- if Value_parameters.NumerorsLogFile.is_known () then
+ if not (Value_parameters.NumerorsLogFile.is_empty ()) then
match f with
| `Value _ ->
let log = open_out (Value_parameters.NumerorsLogFile.get ():>string) in
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 2bbf0cd78e37082fe2fcc87b895ca1e61ef5973d..cd194c77d7a2ef18a4cc3bb67e224939e2e56e04 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -190,4 +190,4 @@ let output file =
Format.fprintf fmt "@]%!"
let report () =
- Value_parameters.ReportRedStatuses.(if is_known () then output (get ()))
+ 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 45c937f301374a216138302e3b9f5370fbb8490d..b4c455f6db589faaba2a24fbf63646b29526febf 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -395,7 +395,7 @@ let start_doing_flamegraph callstack =
| [] -> assert false
| [_] ->
(* Analysis of main *)
- if Value_parameters.ValPerfFlamegraphs.is_known () 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 *)
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);