diff --git a/Makefile b/Makefile
index b99afea518b664558478423dade71ea554e0a325..90d05c020d39381a0b657499a5447d421b06850d 100644
--- a/Makefile
+++ b/Makefile
@@ -857,7 +857,7 @@ endif
# General rules for ordering files within PLUGIN_CMO:
# - try to keep the legacy Value before Eva
-PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
+PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
utils/eva_audit utils/value_perf utils/eva_annotations \
utils/eva_dynamic utils/value_util utils/red_statuses \
utils/mark_noresults \
@@ -932,7 +932,7 @@ PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
# Eva API.
API_MLI := $(addprefix $(PLUGIN_DIR)/, \
engine/analysis.mli utils/results.mli \
- value_parameters.mli utils/eva_annotations.mli \
+ parameters.mli utils/eva_annotations.mli \
eval.mli domains/cvalue/builtins.mli \
legacy/eval_terms.mli utils/value_results.mli utils/unit_tests.mli)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 4a1d41dd38f7885727b646bf7f65d7a19b4aed76..730ba7179805c2a0447060ea7e9fe6bf50016dfc 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1506,8 +1506,10 @@ src/plugins/value/utils/widen.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/widen.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/widen_hints_ext.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/widen_hints_ext.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/value_parameters.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/value_parameters.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/parameters.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/parameters.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/self.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/self.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/abstract_location.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/abstract_value.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/values/cvalue_backward.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index f95b747b5e7e9ce175417d44afa1832b6d2f3f62..d4bb1d87ba568da2b4e8b1c373cd6520622be0c7 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -80,7 +80,7 @@ let add_slevel_annotations () =
let add_partitioning varname =
match Data_for_aorai.get_varinfo_option varname with
| None -> ()
- | Some vi -> Eva.Value_parameters.use_global_value_partitioning vi
+ | Some vi -> Eva.Parameters.use_global_value_partitioning vi
let add_state_variables_partitioning () =
add_partitioning Data_for_aorai.curState;
diff --git a/src/plugins/markdown-report/eva_info.ml b/src/plugins/markdown-report/eva_info.ml
index b0a59dc172472ee3f611be9e4c075057457e46ba..6fccda29a384d8ec9a3cd25a7bab46eb610ae5c7 100644
--- a/src/plugins/markdown-report/eva_info.ml
+++ b/src/plugins/markdown-report/eva_info.ml
@@ -231,7 +231,7 @@ let coverage_md_gen () =
[ Block [Text summary_whole]; Block [Text summary ]]
let domains_md_gen () =
- let eva_domains = Eva.Value_parameters.enabled_domains () in
+ let eva_domains = Eva.Parameters.enabled_domains () in
let domains = List.filter (fun (name, _) -> name <> "cvalue") eva_domains in
let aux (name, descr) = (plain "domain" @ bold name), plain descr in
List.map aux domains
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 58006b2c451753ca0a1707acada914bcd5106ac6..b3cc902d839a9b3d8c731ded983cf1b3ecd8acb4 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -6,7 +6,7 @@
and memory locations of lvalues at each program point.
The following modules allow configuring the Eva analysis:
- - Value_parameters: change the configuration of the analysis.
+ - Parameters: change the configuration of the analysis.
- Eva_annotations: add local annotations to guide the analysis.
- Builtins: register ocaml builtins to be used by the cvalue domain
instead of analysing the body of some C functions.
@@ -300,7 +300,7 @@ module Results: sig
end
-module Value_parameters: sig
+module Parameters: sig
(** Configuration of the analysis. *)
(** Returns the list (name, descr) of currently enabled abstract domains. *)
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index e65daf45024938b8589daf977653a1725fbe491c..e6ce2b905c4024e602c04268a19a73cf742a036b 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -180,7 +180,7 @@ let combine s1 s2 =
this alarm should be consistent. *)
try merge ~combine:true intersect s1 s2
with Inconsistent ->
- Value_parameters.fatal ~current:true
+ Self.fatal ~current:true
"Inconsistent combination of two alarm maps %a and %a."
pretty s1 pretty s2
@@ -426,14 +426,14 @@ let emit_alarms kinstr map =
let list = M.bindings map in
let sorted_list = List.sort cmp list in
List.iter (fun (alarm, status) -> emit_alarm kinstr alarm status) sorted_list;
- if Alarm_cache.length () >= Value_parameters.StopAtNthAlarm.get ()
- then Value_parameters.abort "Stopping at nth alarm"
+ if Alarm_cache.length () >= Parameters.StopAtNthAlarm.get ()
+ then Self.abort "Stopping at nth alarm"
let emit kinstr = function
| Just map -> if not (M.is_empty map) then emit_alarms kinstr map
(* TODO: use GADT to avoid this assert false ? *)
| AllBut _ ->
- Value_parameters.abort ~current:true ~once:true
+ Self.abort ~current:true ~once:true
"All alarms may arise: \
abstract state too imprecise to continue the analysis."
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index dcd64ed822256755b0a1ccbd1517ca56cc11a8b4..fcb5b3083f08585924b0555529a6a3f52c0c25bb 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -467,8 +467,8 @@ module type S = sig
include Reuse with type t := t
(** Category for the messages about the domain.
- Must be created through {!Value_parameters.register_category}. *)
- val log_category : Value_parameters.category
+ Must be created through {!Self.register_category}. *)
+ val log_category : Self.category
(** This function is called after the analysis. The argument is the state
computed at the return statement of the main function. The function can
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 02df6dedf82d0602cd775295e6e4a5edf5d48c00..c044bc41e10f51e8c93ce2b91960d8b6ff0f05a8 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -24,13 +24,13 @@ open Cil_types
open Eval
open Apron
-let dkey = Value_parameters.register_category "d-apron"
+let dkey = Self.register_category "d-apron"
let debug = false
let abort exclog =
let open Manager in
- Value_parameters.fatal
+ Self.fatal
"Apron manager error : %a in function %a.@.%s"
print_exc exclog.exn print_funid exclog.funid exclog.msg
@@ -151,7 +151,7 @@ let reduce eval expr range =
Since the denominator is not 1, the translation will fail later in
[scalar_to_mpzf]. Thus we should catch this case here. *)
if Interval.is_top interval then begin
- if debug then Value_parameters.result ~current:true ~once:true
+ if debug then Self.result ~current:true ~once:true
"imprecise expr %a" Apron.Texpr1.print_expr expr;
top ()
end
@@ -633,7 +633,7 @@ module Make (Man : Input) = struct
let start_call _stmt call recursion valuation state =
if recursion <> None
then
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"The binding to APRON domains does not support recursive calls.";
update valuation state >>- fun state ->
let eval = make_eval state in
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 6dc0b78d39ac562b844c825419398cb11db4e7b5..6a06c6e95e23e1b5b9f88610ad064028827a0a5d 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -56,7 +56,7 @@ end
module BuiltinsOverride = State_builder.Set_ref (Kernel_function.Set) (Info)
let register_builtin name ?replace ?typ cacheable f =
- Value_parameters.register_builtin name;
+ Parameters.register_builtin name;
let builtin = (name, f, cacheable, typ) in
Hashtbl.replace table name builtin;
match replace with
@@ -84,7 +84,7 @@ let builtin_names_and_replacements () =
let () =
Cmdline.run_after_configuring_stage
(fun () ->
- if Value_parameters.BuiltinsList.get () then begin
+ if Parameters.BuiltinsList.get () then begin
let stand_alone, replacements = builtin_names_and_replacements () in
Log.print_on_output
(fun fmt ->
@@ -152,8 +152,8 @@ let warn_builtin_override kf source bname =
if Kernel_function.is_definition kf && not internal
then
let fname = Kernel_function.get_name kf in
- Value_parameters.warning ~source ~once:true
- ~wkey:Value_parameters.wkey_builtins_override
+ Self.warning ~source ~once:true
+ ~wkey:Self.wkey_builtins_override
"function %s: definition will be overridden by %s"
fname (if fname = bname then "its builtin" else "builtin " ^ bname)
@@ -161,8 +161,8 @@ let prepare_builtin kf (name, builtin, cacheable, expected_typ) =
let source = fst (Kernel_function.get_location kf) in
if inconsistent_builtin_typ kf expected_typ
then
- Value_parameters.warning ~source ~once:true
- ~wkey:Value_parameters.wkey_builtins_override
+ Self.warning ~source ~once:true
+ ~wkey:Self.wkey_builtins_override
"The builtin %s will not be used for function %a of incompatible type.@ \
(got: %a)."
name Kernel_function.pretty kf
@@ -170,8 +170,8 @@ let prepare_builtin kf (name, builtin, cacheable, expected_typ) =
else
match find_builtin_specification kf with
| None ->
- Value_parameters.warning ~source ~once:true
- ~wkey:Value_parameters.wkey_builtins_missing_spec
+ Self.warning ~source ~once:true
+ ~wkey:Self.wkey_builtins_missing_spec
"The builtin for function %a will not be used, as its frama-c libc \
specification is not available."
Kernel_function.pretty kf
@@ -183,7 +183,7 @@ let prepare_builtin kf (name, builtin, cacheable, expected_typ) =
let prepare_builtins () =
BuiltinsOverride.clear ();
Hashtbl.clear builtins_table;
- let autobuiltins = Value_parameters.BuiltinsAuto.get () in
+ let autobuiltins = Parameters.BuiltinsAuto.get () in
(* Links kernel functions to the registered builtins. *)
Hashtbl.iter
(fun name (bname, f, cacheable, typ) ->
@@ -195,7 +195,7 @@ let prepare_builtins () =
with Not_found -> ())
table;
(* Overrides builtins attribution according to the -eva-builtin option. *)
- Value_parameters.BuiltinsOverrides.iter
+ Parameters.BuiltinsOverrides.iter
(fun (kf, name) ->
prepare_builtin kf (Hashtbl.find table (Option.get name)))
@@ -275,11 +275,11 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
process_result call post call_result
with
| Invalid_nb_of_args n ->
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"Invalid number of arguments for builtin %a: %d expected, %d found"
Kernel_function.pretty call.kf n (List.length arguments)
| Outside_builtin_possibilities ->
- Value_parameters.fatal ~current:true
+ Self.fatal ~current:true
"Call to builtin %a failed" Kernel_function.pretty call.kf
(*
diff --git a/src/plugins/value/domains/cvalue/builtins_float.ml b/src/plugins/value/domains/cvalue/builtins_float.ml
index f950c308568da01b587e7d9c0a39c9b333214cc5..71dd8418d093a71a5a7ebcae5981b53eb51cb393 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.ml
+++ b/src/plugins/value/domains/cvalue/builtins_float.ml
@@ -87,7 +87,7 @@ let arity1 name fk caml_fun _state actuals =
if Cvalue.V.is_bottom arg then begin
V.bottom
end else begin
- Value_parameters.result ~once:true ~current:true
+ Self.result ~once:true ~current:true
"function %s applied to address" name;
Cvalue.V.topify_arith_origin arg
end
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index dd27fe5eca32e88f8c9f79e491182deb7a6d29bb..c6197530c239f399dec5a5ddb7f85e2e1e6714b5 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -25,12 +25,12 @@ open Abstract_interp
open Locations
open Cvalue
-let dkey = Value_parameters.register_category "malloc"
+let dkey = Self.register_category "malloc"
-let wkey_weak_alloc = Value_parameters.register_warn_category "malloc:weak"
-let () = Value_parameters.set_warn_status wkey_weak_alloc Log.Winactive
+let wkey_weak_alloc = Self.register_warn_category "malloc:weak"
+let () = Self.set_warn_status wkey_weak_alloc Log.Winactive
-let wkey_imprecise_alloc = Value_parameters.register_warn_category
+let wkey_imprecise_alloc = Self.register_warn_category
"malloc:imprecise"
(* ---------------------- Dynamically allocated bases ----------------------- *)
@@ -68,7 +68,7 @@ let current_call_site () =
let call_stack_no_wrappers () =
let stack = Value_util.call_stack () in
assert (stack != []);
- let wrappers = Value_parameters.AllocFunctions.get() in
+ let wrappers = Parameters.AllocFunctions.get() in
let rec bottom_filter = function
| [] -> assert false
| [_] as stack -> stack (* Do not empty the stack completely *)
@@ -165,7 +165,7 @@ let create_new_var stack prefix type_base weak =
created by one of the functions of this module. Mutating variables name
is not a good idea in general, but we take the risk here. *)
let mutate_name_to_weak vi =
- Value_parameters.warning ~wkey:wkey_weak_alloc ~current:true ~once:false
+ Self.warning ~wkey:wkey_weak_alloc ~current:true ~once:false
"@[marking variable `%s' as weak@]%t" vi.vname
Value_util.pp_callstack;
try
@@ -299,7 +299,7 @@ let add_zeroes = add_v (V_Or_Uninitialized.initialized Cvalue.V.singleton_zero)
[returns_null]: if given, forces the result to consider/ignore the
possibility of failure, despite -eva-alloc-returns-null. *)
let wrap_fallible_alloc ?returns_null ret orig_state state_after_alloc =
- let default_returns_null = Value_parameters.AllocReturnsNull.get () in
+ let default_returns_null = Parameters.AllocReturnsNull.get () in
let returns_null = Option.value ~default:default_returns_null returns_null in
let success = Some ret, state_after_alloc in
if returns_null
@@ -325,7 +325,7 @@ let alloc_fresh weak deallocation prefix sizev _state =
let tsize = guess_intended_malloc_type stack sizev (weak = Strong) in
let type_base = type_from_nb_elems tsize in
let var = create_new_var stack prefix type_base weak in
- Value_parameters.result ~current:true ~once:true
+ Self.result ~current:true ~once:true
"@[allocating %svariable %a@]%t"
(if weak = Weak then "weak " else "") Printer.pp_varinfo var
Value_util.pp_callstack;
@@ -384,7 +384,7 @@ let create_weakest_base region =
TArray (Cil.charType, None, [])
in
let var = create_new_var stack "alloc" type_base Weak in
- Value_parameters.warning ~wkey:wkey_imprecise_alloc ~current:true ~once:true
+ Self.warning ~wkey:wkey_imprecise_alloc ~current:true ~once:true
"allocating a single weak variable for ALL dynamic allocations %s: %a"
(string_of_region region) Printer.pp_varinfo var;
let min_alloc = Int.minus_one in
@@ -434,7 +434,7 @@ let update_variable_validity ?(make_weak=false) base sizev =
if not (Int.equal variable_v.Base.min_alloc min_sure_bits) ||
not (Int.equal variable_v.Base.max_alloc max_valid_bits)
then begin
- Value_parameters.result ~dkey ~current:true ~once:false
+ Self.result ~dkey ~current:true ~once:false
"@[resizing variable `%a'@ (%a) to fit %a@]"
Printer.pp_varinfo vi
pp_validity (variable_v.Base.min_alloc, variable_v.Base.max_alloc)
@@ -447,11 +447,11 @@ let update_variable_validity ?(make_weak=false) base sizev =
Base.update_variable_validity variable_v
~weak:make_weak ~min_alloc:min_sure_bits ~max_alloc:max_valid_bits;
base, max_valid_bits
- | _ -> Value_parameters.fatal "base is not Allocated: %a" Base.pretty base
+ | _ -> Self.fatal "base is not Allocated: %a" Base.pretty base
let alloc_by_stack region prefix sizev state =
let stack = call_stack_no_wrappers () in
- let max_level = Value_parameters.MallocLevel.get () in
+ let max_level = Parameters.MallocLevel.get () in
let all_vars =
try MallocedByStack.find stack
with Not_found -> []
@@ -635,11 +635,11 @@ let resolve_bases_to_free arg =
let free_aux state ~strong bases_to_remove =
(* TODO: reduce on arg if it is an lval *)
if strong then begin
- Value_parameters.debug ~current:true ~dkey "strong free on bases: %a"
+ Self.debug ~current:true ~dkey "strong free on bases: %a"
Base.Hptset.pretty bases_to_remove;
free ~exact:true bases_to_remove state
end else begin
- Value_parameters.debug ~current:true ~dkey "weak free on bases: %a"
+ Self.debug ~current:true ~dkey "weak free on bases: %a"
Base.Hptset.pretty bases_to_remove;
free ~exact:false bases_to_remove state
end
@@ -692,7 +692,7 @@ let free_automatic_bases stack state =
in
if Base.Hptset.is_empty bases_to_free then state
else begin
- Value_parameters.result ~current:true ~once:true
+ Self.result ~current:true ~once:true
"freeing automatic bases: %a" Base.Hptset.pretty bases_to_free;
let state', _changed = free_aux state ~strong:true bases_to_free in
(* TODO: propagate 'freed' bases for From? *)
@@ -738,7 +738,7 @@ let realloc_copy_one size ~src_state ~dst_state new_base b =
be created: if [Weak], convergence is ensured using a malloc builtin
that converges. If [Strong], a new base is created for each call. *)
let realloc_alloc_copy weak bases_to_realloc null_in_arg sizev state =
- Value_parameters.debug ~dkey "bases_to_realloc: %a"
+ Self.debug ~dkey "bases_to_realloc: %a"
Base.Hptset.pretty bases_to_realloc;
assert (not (Model.(equal state bottom || equal state top)));
let _size_valid, size_max = extract_size sizev in (* bytes everywhere *)
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index 6309adb64fb18947419e58d53a12c82ffc069644..d40cc1db42d8b7f6a3dc2d9bf6765a5715448c1f 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -28,7 +28,7 @@ open Locations
let register_builtin name ?replace builtin =
Builtins.register_builtin name ?replace Cacheable builtin
-let dkey = Value_parameters.register_category "imprecision"
+let dkey = Self.register_category "imprecision"
let frama_C_is_base_aligned _state = function
| [_, x; _, y] ->
@@ -58,7 +58,7 @@ let frama_c_offset _state = function
let offsets = Location_Bytes.fold_i (fun _b -> Ival.join) x acc in
Cvalue.V.inject_ival offsets
with Abstract_interp.Error_Top ->
- Value_parameters.error ~current:true
+ Self.error ~current:true
"Builtin Frama_C_offset is applied to a value not \
guaranteed to be an address";
Cvalue.V.top_int
@@ -75,7 +75,7 @@ exception Indeterminate of V_Or_Uninitialized.t
(* Called by the [memcpy] builtin. Warns when the offsetmap contains
an indeterminate value, when the imprecision category is enabled *)
let memcpy_check_indeterminate_offsetmap offsm =
- if Value_parameters.is_debug_key_enabled dkey then
+ if Self.is_debug_key_enabled dkey then
try
let aux_offset _ (v, _, _) =
match v with
@@ -84,7 +84,7 @@ let memcpy_check_indeterminate_offsetmap offsm =
in
V_Offsetmap.iter aux_offset offsm
with Indeterminate v ->
- Value_parameters.debug ~current:true ~dkey ~once:true
+ Self.debug ~current:true ~dkey ~once:true
"@[In memcpy@ builtin:@ precise@ copy of@ indeterminate@ values %a@]%t"
V_Or_Uninitialized.pretty v Value_util.pp_callstack
@@ -101,7 +101,7 @@ let deps_nth_arg n =
let frama_c_memcpy state actuals =
let compute (_exp_dst,dst_bytes) (_exp_src,src_bytes) (_exp_size,size) =
- let plevel = Value_parameters.ArrayPrecisionLevel.get() in
+ let plevel = Parameters.ArrayPrecisionLevel.get() in
let size =
try Cvalue.V.project_ival size
with Cvalue.V.Not_based_on_null -> Ival.top (* TODO: use size_t *)
@@ -229,7 +229,7 @@ let frama_c_memcpy state actuals =
raise (Memcpy_result (state,c_from,sure_zone))
with
| Abstract_interp.Not_less_than ->
- Value_parameters.debug ~dkey ~once:true
+ Self.debug ~dkey ~once:true
~current:true "In memcpy builtin: too many sizes to enumerate, \
possible loss of precision";
(* Too many slices in the size. We read the entire range
@@ -240,7 +240,7 @@ let frama_c_memcpy state actuals =
in
begin match v with
| V_Or_Uninitialized.C_init_noesc _ -> ()
- | _ -> Value_parameters.result ~dkey ~current:true ~once:true
+ | _ -> Self.result ~dkey ~current:true ~once:true
"@[In memcpy@ builtin:@ imprecise@ copy of@ indeterminate@ values@]%t"
Value_util.pp_callstack
end;
@@ -600,7 +600,7 @@ let frama_c_memset state actuals =
in
try frama_c_memset_precise state dst v (exp_size, size)
with ImpreciseMemset reason ->
- Value_parameters.debug ~dkey ~current:true
+ Self.debug ~dkey ~current:true
"Call to builtin precise_memset(%a) failed; %a%t"
Value_util.pretty_actuals actuals pretty_imprecise_memset_reason reason
Value_util.pp_callstack;
@@ -627,7 +627,7 @@ let frama_c_interval_split _state actuals =
with
| Cvalue.V.Not_based_on_null
| Ival.Not_Singleton_Int ->
- Value_parameters.abort
+ Self.abort
"Invalid call to Frama_C_interval_split%a"
Value_util.pretty_actuals actuals
end
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index d73d76bde382eb383e0563235a544ff8801e88e9..362838cec970a39af6e6f380aafcf0fe3ca4fcb2 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -216,7 +216,7 @@ let value_pretty cas print_ampamp lv s_bytes fmt v =
else find_typ_assignment candidate_types
with
| V.Not_based_on_null -> ()
- | Not_found -> Value_parameters.result "Unknown size %d for %s" s_bytes lv
+ | Not_found -> Self.result "Unknown size %d for %s" s_bytes lv
let value_uninit_pretty cas prampamp lv s fmt = function
@@ -282,7 +282,7 @@ let state_pretty cas fmt m =
with
| Z.Overflow
| Too_large_to_enumerate ->
- Value_parameters.warning "base %s too large, \
+ Self.warning "base %s too large, \
will not print it" name
end
| _ -> ())
@@ -323,14 +323,14 @@ let pretty_state_as_c_assignments fmt state =
let frama_c_dump_assert state _actuals =
- Value_parameters.result ~current:true "Frama_C_dump_assert_each called:@\n(%a)@\nEnd of Frama_C_dump_assert_each output"
+ Self.result ~current:true "Frama_C_dump_assert_each called:@\n(%a)@\nEnd of Frama_C_dump_assert_each output"
pretty_state_as_c_assert state;
Builtins.States [state]
let () = Builtins.register_builtin "Frama_C_dump_assert_each" NoCache frama_c_dump_assert
let frama_c_dump_assignments state _actuals =
- Value_parameters.result ~current:true "Frama_C_dump_assignment_each called:@\n%a@\nEnd of Frama_C_dump_assignment_each output"
+ Self.result ~current:true "Frama_C_dump_assignment_each called:@\n%a@\nEnd of Frama_C_dump_assignment_each output"
pretty_state_as_c_assignments state;
Builtins.States [state]
diff --git a/src/plugins/value/domains/cvalue/builtins_split.ml b/src/plugins/value/domains/cvalue/builtins_split.ml
index 1b628c5876a293f554206e1ffe05906b7d8eab6f..b7dbebcb9e52c0973e83c0159a046062888b2236 100644
--- a/src/plugins/value/domains/cvalue/builtins_split.ml
+++ b/src/plugins/value/domains/cvalue/builtins_split.ml
@@ -65,7 +65,7 @@ let () =
let warning warn s =
if warn then
- Value_parameters.result ~current:true ~once:true s
+ Self.result ~current:true ~once:true s
else
Pretty_utils.nullprintf s
@@ -182,13 +182,13 @@ let aux_split f state = function
in
f ~warn:true lv state max_card
with V.Not_based_on_null | Ival.Not_Singleton_Int ->
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"Cannot use non-constant split level %a" V.pretty card;
[state]
in
Builtins.States states
| _ ->
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"Cannot interpret split directive. Ignoring";
Builtins.States [state]
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index 9b74eeb416fd416cf0dd14aae0fea58150fb4d0c..3507dcea92bceb60c5b068076971d8d40c3e6386 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -113,7 +113,7 @@ let watch_hook (stmt, _callstack, states) =
in
if watching
then begin
- Value_parameters.feedback ~once:true ~current:true
+ Self.feedback ~once:true ~current:true
"Watchpoint: %a %a%t"
Printer.pp_exp name
V.pretty vs
@@ -124,7 +124,7 @@ let watch_hook (stmt, _callstack, states) =
else
let current = Integer.pred current in
if Integer.is_zero current then
- Value_parameters.abort "Watchpoint builtin: countdown to zero";
+ Self.abort "Watchpoint builtin: countdown to zero";
w.remaining_count <- current;
w.stmts <- Cil_datatype.Stmt.Set.add stmt set;
end)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index cd9f4376d4ef60a4c288d294eb3bca0ec1345b88..19b81136d700713661d84b482d038e24d2c57448 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -22,7 +22,7 @@
open Eval
-let dkey_card = Value_parameters.register_category "cardinal"
+let dkey_card = Self.register_category "cardinal"
module Model = struct
@@ -161,7 +161,7 @@ module State = struct
type state = Model.t * Locals_scoping.clobbered_set
- let log_category = Value_parameters.dkey_cvalue_domain
+ let log_category = Self.dkey_cvalue_domain
include Datatype.Make_with_collections (
struct
@@ -405,7 +405,7 @@ module State = struct
let bind_local state vi =
let b = Base.of_varinfo vi in
let offsm =
- if Value_parameters.InitializedLocals.get () then
+ if Parameters.InitializedLocals.get () then
let v = Cvalue.(V_Or_Uninitialized.initialized V.top_int) in
match Cvalue.V_Offsetmap.size_from_validity (Base.validity b) with
| `Bottom -> assert false
@@ -525,7 +525,7 @@ module State = struct
if Cvalue.Model.is_reachable fst_values
&& not (Cvalue.Model.is_top fst_values)
then begin
- let print_cardinal = Value_parameters.is_debug_key_enabled dkey_card in
+ let print_cardinal = Self.is_debug_key_enabled dkey_card in
let estimate =
if print_cardinal
then Cvalue.Model.cardinal_estimate values
@@ -551,22 +551,22 @@ module State = struct
| _ -> ())
(fun fmt -> Cvalue.Model.pretty_filter fmt values outs) in
match fmt with
- | None -> Value_parameters.printf
- ~dkey:Value_parameters.dkey_final_states ~header "%t" body
+ | None -> Self.printf
+ ~dkey:Self.dkey_final_states ~header "%t" body
| Some fmt -> Format.fprintf fmt "%t@.%t@," header body
end
with Kernel_function.No_Statement -> ()
let display_results () =
- Value_parameters.result "====== VALUES COMPUTED ======";
+ Self.result "====== VALUES COMPUTED ======";
Eva_dynamic.Callgraph.iter_in_rev_order display;
- Value_parameters.result "%t" Value_perf.display
+ Self.result "%t" Value_perf.display
let post_analysis _state =
- if Value_parameters.ForceValues.get ()
- && Value_parameters.verbose_atleast 1
+ if Parameters.ForceValues.get ()
+ && Self.verbose_atleast 1
&& Plugin.is_present "inout"
- then Value_parameters.ForceValues.output display_results
+ then Parameters.ForceValues.output display_results
end
let () = Db.Value.display := (fun fmt kf -> State.display ~fmt kf)
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index 4faee93725faf82ad6fc7c6ee1cf5f88ca332381..ee6a2bbebbba3f420d8878ae0c161d322e4bb875 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -25,7 +25,7 @@
open Cil_types
open Locations
-let dkey = Value_parameters.register_category "initial-state"
+let dkey = Self.register_category "initial-state"
let add_initialized state loc v =
Cvalue.Model.add_binding ~exact:true state loc v
@@ -45,8 +45,8 @@ let make_well hidden_base state loc =
let warn_unknown_size_aux pp v (messt, t) =
- Value_parameters.warning ~once:true ~current:true
- ~wkey:Value_parameters.wkey_unknown_size
+ Self.warning ~once:true ~current:true
+ ~wkey:Self.wkey_unknown_size
"@[during initialization@ of %a,@ size of@ type '%a'@ cannot be@ computed@ \
(%s)@]" pp v Printer.pp_typ t messt
@@ -75,7 +75,7 @@ let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
in
match validity with
| Base.Known (a,b)
- when not (Value_parameters.AllocatedContextValid.get ()) ->
+ when not (Parameters.AllocatedContextValid.get ()) ->
(* Weaken validity, because the created variables are not supposed
to be valid *)
(match valid with
@@ -86,7 +86,7 @@ let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
| UnknownValidity -> Base.Unknown (a, None, b)
)
| Base.Unknown _ -> (* Unknown validity is caused by strange type *)
- Value_parameters.result ~dkey "creating variable %s with imprecise \
+ Self.result ~dkey "creating variable %s with imprecise \
size (type %a)" hidden_var_name Printer.pp_typ pointed_typ;
validity
| Base.Empty | Base.Known _ | Base.Invalid -> validity
@@ -100,7 +100,7 @@ let reject_empty_struct b offset typ =
match Cil.unrollType typ with
| TComp (ci, _) ->
if ci.cfields = Some [] && not (Cil.acceptEmptyCompinfo ()) then
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"@[empty %ss@ are unsupported@ (type '%a',@ location %a%a)@ \
in C99 (only allowed on GCC/MSVC machdep).@ Aborting.@]"
(if ci.cstruct then "struct" else "union")
@@ -131,11 +131,11 @@ let initialize_var_using_type varinfo state =
| TFun _ -> state
| TPtr (typ, _) as full_typ
- when depth <= Value_parameters.AutomaticContextMaxDepth.get () ->
+ when depth <= Parameters.AutomaticContextMaxDepth.get () ->
let attr = Cil.typeAttrs full_typ in
let libc = Cil.is_in_libc varinfo.vattr in
let context_max_width =
- Value_parameters.AutomaticContextMaxWidth.get ()
+ Parameters.AutomaticContextMaxWidth.get ()
in begin
match Cil.isVoidType typ, Cil.isFunctionType typ with
| false, false -> (* non-void, non-function *)
@@ -176,7 +176,7 @@ let initialize_var_using_type varinfo state =
in
let value = Cvalue.V.inject hidden_base (Ival.zero) in
let value =
- if Value_parameters.AllocatedContextValid.get ()
+ if Parameters.AllocatedContextValid.get ()
then value
else Cvalue.V.join Cvalue.V.singleton_zero value
in
@@ -204,7 +204,7 @@ let initialize_var_using_type varinfo state =
let state = ref state in
let typ = Cil.unrollType typ in
let max_precise_size =
- Value_parameters.AutomaticContextMaxWidth.get ()
+ Parameters.AutomaticContextMaxWidth.get ()
in
let locs = ref [] in
for i = 0 to min psize (pred max_precise_size) do
@@ -272,7 +272,7 @@ let initialize_var_using_type varinfo state =
(* We have probably initialized a struct with different fields.
We must perform offsetmap copies, that are slower *)
if nb_fields * psize >= 5000 then
- Value_parameters.result ~once:true ~current:true
+ Self.result ~once:true ~current:true
"Initializing a complex array of %d elements. This may \
take some time" size;
let loc = ref last_loc.loc in
@@ -288,7 +288,7 @@ let initialize_var_using_type varinfo state =
!state
with
| Cil.LenOfArray cause ->
- Value_parameters.result ~once:true ~current:true
+ Self.result ~once:true ~current:true
"problem with array size (%a), assuming 0"
Cil.pp_incorrect_array_length cause;
(* This is either a flexible array member (for which Cil
@@ -326,7 +326,7 @@ let initialize_var_using_type varinfo state =
(* Union of arithmetic types *)
bind_entire_loc Cvalue.V.top_int
- | TPtr _ when Value_parameters.AllocatedContextValid.get () ->
+ | TPtr _ when Parameters.AllocatedContextValid.get () ->
(* deep pointers map to NULL in this case *)
bind_entire_loc Cvalue.V.singleton_zero
diff --git a/src/plugins/value/domains/cvalue/cvalue_specification.ml b/src/plugins/value/domains/cvalue/cvalue_specification.ml
index fdedf776bb94083159a966c7c9085b5e978c1ccd..ac5b5396cab61c311f75e2c48fd0c1e4f76fc121 100644
--- a/src/plugins/value/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_specification.ml
@@ -66,7 +66,7 @@ let check_from pre_state asgn assigns_zone from found_froms =
let found_direct_deps = found_deps.Function_Froms.Deps.data in
let found_indirect_deps = found_deps.Function_Froms.Deps.indirect in
let res_for_unknown txt =
- Value_parameters.debug "found_direct deps %a stated_direct_deps %a \
+ Self.debug "found_direct deps %a stated_direct_deps %a \
found_indirect_deps %a stated_indirect_deps %a"
Zone.pretty found_direct_deps Zone.pretty stated_direct_deps
Zone.pretty found_indirect_deps Zone.pretty stated_indirect_deps;
@@ -84,12 +84,12 @@ let check_from pre_state asgn assigns_zone from found_froms =
(* Display the message as result/warning depending on [status] *)
let msg_status status ?current ?once ?source fmt =
if status = Alarmset.True then
- if Value_parameters.ValShowProgress.get ()
- then Value_parameters.result ?current ?once ?source fmt
- else Value_parameters.result ?current ?once ?source ~level:2 fmt
+ if Parameters.ValShowProgress.get ()
+ then Self.result ?current ?once ?source fmt
+ else Self.result ?current ?once ?source ~level:2 fmt
else
- Value_parameters.warning
- ~wkey:Value_parameters.wkey_alarm ?current ?once ?source fmt
+ Self.warning
+ ~wkey:Self.wkey_alarm ?current ?once ?source fmt
let pp_bhv fmt b =
if not (Cil.is_default_behavior b)
@@ -139,7 +139,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
let status_txt, vstatus, status =
if not (Zone.is_included outputs assigns_union)
then (
- Value_parameters.debug
+ Self.debug
"@[Cannot prove assigns clause@]@ \
@[<2>found assigns: %a@]@ @[<2>stated assigns: %a@]"
Zone.pretty outputs Zone.pretty assigns_union;
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 59adfa1136bf985c422ea254a7eacaf2c33c9e01..874865e8abae16d543aece59090cc1dd8e36cae9 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -98,10 +98,10 @@ let write_abstract_value state (lval, loc, typ) assigned_value =
in
match loc.Locations.loc with
| Locations.Location_Bits.Top (Base.SetLattice.Top, orig) ->
- Value_parameters.result
+ Self.result
"State before degeneration:@\n======%a@\n======="
Cvalue.Model.pretty state;
- Value_parameters.fatal ~current:true
+ Self.fatal ~current:true
"writing at a completely unknown address@[%a@].@\nAborting."
Origin.pretty_as_reason orig
| _ ->
diff --git a/src/plugins/value/domains/cvalue/warn.ml b/src/plugins/value/domains/cvalue/warn.ml
index 9f931b0f3c75ab5baf3b8161250f52f08d613e2a..0ac785c335db88a8a994f2b836e415bc7d96160b 100644
--- a/src/plugins/value/domains/cvalue/warn.ml
+++ b/src/plugins/value/domains/cvalue/warn.ml
@@ -27,14 +27,14 @@ let warn_locals_escape is_block fundec k locals =
let pretty_base = Base.pretty in
let pretty_block fmt = Pretty_utils.pp_cond is_block fmt "a block of " in
let sv = fundec.svar in
- Value_parameters.warning
- ~wkey:Value_parameters.wkey_locals_escaping
+ Self.warning
+ ~wkey:Self.wkey_locals_escaping
~current:true ~once:true
"locals %a escaping the scope of %t%a through %a"
Base.Hptset.pretty locals pretty_block Printer.pp_varinfo sv pretty_base k
let warn_imprecise_lval_read lv loc contents =
- if Value_parameters.verbose_atleast 1 then
+ if Self.verbose_atleast 1 then
let pretty_gm fmt s =
let s = Base.SetLattice.(inject (O.remove Base.null s)) in
Base.SetLattice.pretty fmt s
@@ -62,7 +62,7 @@ let warn_imprecise_lval_read lv loc contents =
in
if something_to_warn
then
- Value_parameters.result ~current:true ~once:true
+ Self.result ~current:true ~once:true
"@[<v>@[Reading left-value %a.@]@ %t%t%t@]"
Printer.pp_lval lv
(fun fmt ->
@@ -100,7 +100,7 @@ let warn_imprecise_lval_read lv loc contents =
let warn_right_exp_imprecision lv loc_lv exp_val =
match exp_val with
| Location_Bytes.Top(_topparam,origin) ->
- Value_parameters.result ~once:true ~current:true
+ Self.result ~once:true ~current:true
"@[<v>@[Assigning imprecise value to %a%t.@]%a%t@]"
Printer.pp_lval lv
(fun fmt -> match lv with
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 24a1b2effb86cb319813b9cbdc7826ba8f50e04f..8505c33b87e56f450f9079ec43491aa8d4682982 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -106,7 +106,7 @@ module Make_Minimal
include Domain
- let log_category = Value_parameters.register_category ("d-" ^ name)
+ let log_category = Self.register_category ("d-" ^ name)
type value = Value.t
type location = Location.location
@@ -132,7 +132,7 @@ module Make_Minimal
| None -> `Value (Domain.start_call stmt (simplify_call call) state)
| Some _ ->
(* TODO *)
- Value_parameters.abort
+ Self.abort
"The domain %s does not support recursive call." Domain.name
let finalize_call stmt call recursion ~pre ~post =
@@ -217,7 +217,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
(Domain) (struct let module_name = Domain.name end)
: Datatype.S_with_collections with type t := t)
- let log_category = Value_parameters.register_category ("d-" ^ name)
+ let log_category = Self.register_category ("d-" ^ name)
type value = Cvalue.V.t
type location = Precise_locs.precise_location
@@ -258,7 +258,7 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
| None -> `Value (Domain.start_call stmt call (record valuation) state)
| Some _ ->
(* TODO *)
- Value_parameters.abort
+ Self.abort
"The domain %s does not support recursive call." Domain.name
let finalize_call stmt call recursion =
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 3069d90b752a5aee918f5169532921b8d364e705..ef11c0a44abca4a45b4e6d432b7dac742d89e624 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -24,7 +24,7 @@ open Eval
let counter = ref 0
-let product_category = Value_parameters.register_category "domain_product"
+let product_category = Self.register_category "domain_product"
module Make
(Value: Abstract_value.S)
@@ -174,7 +174,7 @@ module Make
let show_expr =
let (|-) f g = fun fmt exp -> f fmt exp; g fmt exp in
let show_expr_one_side category name show_expr = fun fmt exp ->
- if Value_parameters.is_debug_key_enabled category
+ if Self.is_debug_key_enabled category
then Format.fprintf fmt "@,@]@[<v># %s: @[<hov>%a@]" name show_expr exp
in
let right_log = Right.log_category
@@ -204,7 +204,7 @@ module Make
let pretty =
let print_one_side fmt category name dump state =
- if Value_parameters.is_debug_key_enabled category
+ if Self.is_debug_key_enabled category
then Format.fprintf fmt "# %s:@ @[<hv>%a@]@ " name dump state
in
let right_log = Right.log_category
diff --git a/src/plugins/value/domains/domain_product.mli b/src/plugins/value/domains/domain_product.mli
index 49ca1c6a62b2deb26400060de5a11a55929c08a8..8e5a3b9de23e5dcbe01d18549d5a9338d8304414 100644
--- a/src/plugins/value/domains/domain_product.mli
+++ b/src/plugins/value/domains/domain_product.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-val product_category: Value_parameters.category
+val product_category: Self.category
module Make
(Value: Abstract_value.S)
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index ddf7bae272b9a77f854c3f3adac277e14ade6602..a237f1f912278e6a5b8898af183dcccba337333c 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -30,8 +30,8 @@ type call_init_state =
let call_init_state kf =
let str =
- try Value_parameters.EqualityCallFunction.find kf
- with Not_found -> Value_parameters.EqualityCall.get ()
+ try Parameters.EqualityCallFunction.find kf
+ with Not_found -> Parameters.EqualityCall.get ()
in
match str with
| "all" -> ISCaller
@@ -39,7 +39,7 @@ let call_init_state kf =
| "none" -> ISEmpty
| _ -> assert false
-let dkey = Value_parameters.register_category "d-equality"
+let dkey = Self.register_category "d-equality"
open Hcexprs
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index c51111bbd3f1a9f4c8f8806c203b9e4a15971928..4960424c455ed43c95643543a65a100c340bff8e 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1108,7 +1108,7 @@ module G = struct
end
-let dkey = Value_parameters.register_category "d-gauges"
+let dkey = Self.register_category "d-gauges"
module D : Abstract_domain.Leaf
with type state = G.t
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 946b34461d059ea28d0c5cbc00a844d411cb9ef8..87f4ac0fa15bfa9fdfd9471c56cc20058cc517bd 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -222,7 +222,7 @@ module D
include Domain_builder.Complete (LatticeInout)
- let log_category = Value_parameters.register_category "d-inout"
+ let log_category = Self.register_category "d-inout"
let enter_scope _kind _vars state = state
let leave_scope _kf vars state = Transfer.remove_variables vars state
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 90abdbb2f7bdaa9de528c55ec6cdeedf28a25d4b..f7c5a591d739519341fa3c3a7505617fa820eff2 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -23,7 +23,7 @@
open Cil_types
open Eval
-let dkey = Value_parameters.register_category "d-multidim"
+let dkey = Self.register_category "d-multidim"
let map_to_singleton map =
let aux base offset = function
@@ -451,7 +451,7 @@ struct
let start_call _stmt call recursion valuation state =
if recursion <> None
then
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"The multidim domain does not support recursive calls yet";
let oracle = make_oracle valuation in
let bind state arg =
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
index eaec32fbb9f436c37b2580dddcd6f49e080fdfa3..b5ed4180e900c0a8fc648f54fca9d220fef63cfd 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -86,10 +86,10 @@ module Domain = struct
include Simple_memory.Make_Domain (Name) (Numerors_Value)
let post_analysis f =
- if not (Value_parameters.NumerorsLogFile.is_empty ()) then
+ if not (Parameters.NumerorsLogFile.is_empty ()) then
match f with
| `Value _ ->
- let log = open_out (Value_parameters.NumerorsLogFile.get ():>string) in
+ let log = open_out (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
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index f44600a260c0819b362f33a4e16e58a5059e9484..79d4426df919c2d24adbd2710828548fbdc41a48 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -42,7 +42,7 @@ let saturate_octagons = true
option. In this case, the analysis of each function starts with an empty
state, and the relations inferred in a function are not propagated back to
the caller either. *)
-let intraprocedural () = not (Value_parameters.OctagonCall.get ())
+let intraprocedural () = not (Parameters.OctagonCall.get ())
(* -------------------------------------------------------------------------- *)
(* Basic types: pair of variables and Ival.t *)
@@ -732,7 +732,7 @@ module State = struct
Format.fprintf fmt "@[%a@]" Octagons.pretty octagons
end)
- let log_category = Value_parameters.register_category "d-octagon"
+ let log_category = Self.register_category "d-octagon"
let pretty_debug fmt { octagons; intervals; relations } =
Format.fprintf fmt "@[<v> Octagons: %a@; Intervals: %a@; Relations: %a@]"
@@ -758,7 +758,7 @@ module State = struct
if Octagons.for_all check_octagon t.octagons
then t
else
- Value_parameters.abort
+ Self.abort
"Incorrect octagon state computed by function %s:@ %a"
msg pretty_debug t
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 235d98ba9909b29645acd381f1348c3704a07685..a05dc30f5f2c7bd14b3285e4a1a4606f81a9d68f 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -30,7 +30,7 @@ let store_redundant = false
unsoundnesses in the domain through testing, because many more expressions
end up being handled. *)
-let dkey = Value_parameters.register_category "d-bitwise"
+let dkey = Self.register_category "d-bitwise"
module Default_offsetmap = struct
open Cvalue
diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml
index 0be9f3fb61d85bd030a328335354874f295f89e8..e899e14a70d41870f7ffe1dc9281c2a0ff1366fa 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -27,7 +27,7 @@ open Eval
what goes through it. *)
module Simple : Simpler_domains.Simple_Cvalue = struct
- let feedback = Value_parameters.feedback ~current:true
+ let feedback = Self.feedback ~current:true
(* --- Datatype --- *)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index fa09688306a1d5aff2d62bad75740884394c2306..70a77a3f08af796ea1dd34ffa65c0c65b3579f7c 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -196,7 +196,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
type location = Precise_locs.precise_location
type origin
- let log_category = Value_parameters.register_category ("d-" ^ Info.name)
+ let log_category = Self.register_category ("d-" ^ Info.name)
let widen _kf _stmt = widen
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index b787c686b12e2763f8988d99d1d28ab7bee6a3dc..65cdb97b9a767a3eba9907b1b74cb2a904cd9864 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -24,7 +24,7 @@ open Cil_types
open Eval
open Locations
-let dkey = Value_parameters.register_category "d-symblocs"
+let dkey = Self.register_category "d-symblocs"
module K = Hcexprs
module V = Cvalue.V (* TODO: functorize (with locations too ?) *)
@@ -275,7 +275,7 @@ module Memory = struct
let z =
try K2Z.find k state.zones
with Not_found ->
- Value_parameters.abort "Missing zone for %a@.%a"
+ Self.abort "Missing zone for %a@.%a"
K.HCE.pretty k pretty state
in
add_deps k v z acc
@@ -489,7 +489,7 @@ module D : Abstract_domain.Leaf
| `Value loc -> loc.Eval.loc
in
if Precise_locs.(equal_loc loc_top r) then
- Value_parameters.fatal "Unknown location for %a" Printer.pp_lval lv
+ Self.fatal "Unknown location for %a" Printer.pp_lval lv
else r
let get_val valuation = fun lv ->
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index c4ab2b01ecc7fbb25a10f70ab7e85aab6ee9046d..8ba90e4ceb9317f1afc05a983318d3963951d4a9 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -41,13 +41,13 @@ type taint = {
dependent_call: bool;
}
-let dkey = Value_parameters.register_category "d-taint"
+let dkey = Self.register_category "d-taint"
(* Debug key to also include [assume_stmts] in the output of the
Frama_C_domain_show_each directive. *)
-let dkey_debug = Value_parameters.register_category "d-taint-debug"
+let dkey_debug = Self.register_category "d-taint-debug"
-let wkey = Value_parameters.register_warn_category "taint"
+let wkey = Self.register_warn_category "taint"
module LatticeTaint = struct
@@ -93,7 +93,7 @@ module LatticeTaint = struct
let equal = Datatype.from_compare
let pretty fmt t =
- if Value_parameters.is_debug_key_enabled dkey_debug
+ if Self.is_debug_key_enabled dkey_debug
then pp_state fmt t
else pp_locs_only fmt t
@@ -507,14 +507,14 @@ module TaintLogic = struct
let taint_term taint term =
match eval_tlval_zone cvalue_env term with
| None ->
- Value_parameters.warning ~wkey ~current:true ~once:true
+ Self.warning ~wkey ~current:true ~once:true
"Cannot evaluate term %a in taint annotation; ignoring."
Printer.pp_term term;
taint
| Some (under, over) ->
if not (Zone.equal under over)
then
- Value_parameters.warning ~wkey ~current:true ~once:true
+ Self.warning ~wkey ~current:true ~once:true
"Cannot precisely evaluate term %a in taint annotation; \
over-approximating."
Printer.pp_term term;
@@ -568,7 +568,7 @@ let interpret_taint_logic
in
Abstract.Dom.set key taint state
| _ ->
- Value_parameters.warning ~wkey ~current:true ~once:true
+ Self.warning ~wkey ~current:true ~once:true
"Invalid taint annotation %a; ignoring."
Printer.pp_extended extension;
state
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 88ccb4412c530ed6713e09d7eac5739dbddbde61..4231ef461f95a2f126fcbb1b4e4ea7877635b3c3 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -665,7 +665,7 @@ module Traces = struct
let join c1 c2 =
if c1.call_declared_function <> c2.call_declared_function
then
- Value_parameters.fatal "@[<hv>@[At the same time inside and outside a function call:@]@ %a@ %a@]"
+ Self.fatal "@[<hv>@[At the same time inside and outside a function call:@]@ %a@ %a@]"
pretty c1 pretty c2
else
match view c1, view c2 with
@@ -728,7 +728,7 @@ module Traces = struct
else
Format.printf "@[<hv 2>@[widen %a@]@]@." Stmt.pretty_sid stmt'
end;
- if not (Value_parameters.TracesUnrollLoop.get ())
+ if not (Parameters.TracesUnrollLoop.get ())
then c2
else begin
match c2.current with
@@ -954,7 +954,7 @@ let rec stmts_of_cfg cfg current var_map locals return_exp acc =
Some (exp1, n1', b1, n2')
| _ -> None in
match is_while with
- | None -> Value_parameters.not_yet_implemented "Traces_domain: Loop without condition"
+ | None -> Self.not_yet_implemented "Traces_domain: Loop without condition"
| Some(exp,nloop,bloop,n2) ->
let exp = subst_in_exp var_map exp in
let exp = if bloop then exp else Cil.new_exp ~loc:dummy_loc (UnOp(LNot,exp,Cil.intType)) in
@@ -972,7 +972,7 @@ let rec stmts_of_cfg cfg current var_map locals return_exp acc =
| _ -> None in
let stmt =
match is_if with
- | None -> Value_parameters.not_yet_implemented "Traces_domain: switch at node(%a)" Node.pretty current
+ | None -> Self.not_yet_implemented "Traces_domain: switch at node(%a)" Node.pretty current
| Some(exp,n1,n2) ->
let exp = subst_in_exp var_map exp in
let block1 = Cil.mkBlock (stmts_of_cfg cfg n1 var_map locals return_exp []) in
@@ -1007,7 +1007,7 @@ let project_of_cfg vreturn s =
in
let locals = ref [] in
let graph = match s.current with | Base (_,g) -> g | _ ->
- Value_parameters.fatal "Traces.project_of_cfg used with open loops" in
+ Self.fatal "Traces.project_of_cfg used with open loops" in
let stmts = stmts_of_cfg graph s.start var_map locals return_equal [] in
let sbody = Cil.mkBlock (stmts@[return_stmt]) in
sbody.Cil_types.blocals <- blocals;
@@ -1095,7 +1095,7 @@ module D = struct
include Domain_builder.Complete (Traces)
- let log_category = Value_parameters.register_category "d-traces"
+ let log_category = Self.register_category "d-traces"
let assign ki lv e _v _valuation state =
let trans = Assign (ki, lv.Eval.lval, lv.Eval.ltyp, e) in
@@ -1172,7 +1172,7 @@ module D = struct
let enter_loop stmt state =
let state = Traces.add_trans state (Msg "enter_loop") in
- let state = if not (Value_parameters.TracesUnrollLoop.get ())
+ let state = if not (Parameters.TracesUnrollLoop.get ())
then Traces.add_loop stmt state
else { state with current = UnrollLoop(stmt,state.current) } in
state
@@ -1183,7 +1183,7 @@ module D = struct
| UnrollLoop(_,_) -> state
| OpenLoop(stmt,s,last,_,g,l) ->
let last = Graph.join last g in
- let last = if Value_parameters.TracesUnifyLoop.get () then
+ let last = if Parameters.TracesUnifyLoop.get () then
let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
let last = Graph.join last old_last in
assert (Node.equal s s');
@@ -1203,7 +1203,7 @@ module D = struct
| OpenLoop(stmt,s,last,old_current_node,g,current) ->
assert (Stmt.equal stmt stmt');
let state = { state with current } in
- let last = if Value_parameters.TracesUnifyLoop.get () then
+ let last = if Parameters.TracesUnifyLoop.get () then
let s',old_last = Stmt.Hashtbl.find state.all_loop_start stmt in
let last = Graph.join last old_last in
assert (Node.equal s s');
@@ -1233,7 +1233,7 @@ module D = struct
let output_dot filename state =
let out = open_out filename in
- Value_parameters.feedback ~dkey:log_category "@[Output dot produced to %s.@]" filename;
+ Self.feedback ~dkey:log_category "@[Output dot produced to %s.@]" filename;
(** *)
GraphDot.output_graph out (complete_graph (snd (Traces.get_current state)));
close_out out
@@ -1245,18 +1245,18 @@ module D = struct
| _ -> assert false in
let header fmt = Format.fprintf fmt "Trace domains:" in
let body = Bottom.pretty Traces.pretty in
- Value_parameters.printf ~dkey:log_category ~header " @[%a@]" body state;
- if Value_parameters.TracesProject.get () ||
- not (Value_parameters.TracesDot.is_default ()) then
+ Self.printf ~dkey:log_category ~header " @[%a@]" body state;
+ if Parameters.TracesProject.get () ||
+ not (Parameters.TracesDot.is_default ()) then
match state with
| `Bottom ->
- Value_parameters.failure "The trace is Bottom can't generate code"
+ Self.failure "The trace is Bottom can't generate code"
| `Value state when state ==Traces.top ->
- Value_parameters.failure "The trace is TOP can't generate code"
+ Self.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 ():>string) state;
- if Value_parameters.TracesProject.get ()
+ if not (Parameters.TracesDot.is_default ())
+ then output_dot (Parameters.TracesDot.get ():>string) state;
+ if Parameters.TracesProject.get ()
then project_of_cfg return_exp state
end
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index c3cd5e92da66ddd98fac632153e762e7cfdf52a9..67832adc9449864f073bc6efe263e9ae4af2500e 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-let log_key = Value_parameters.register_category "unit-domain"
+let log_key = Self.register_category "unit-domain"
module Static = struct
module D = struct
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index daa7f30ed177b799041c8f00eb03aca7927a6fa5..f4376aa655175ef30b6cfad5999fe5fbe4a05b82 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -76,7 +76,7 @@ module Config = struct
let register_domain_option ~name ~experimental ~descr =
let descr = if experimental then "Experimental. " ^ descr else descr in
- Value_parameters.register_domain ~name ~descr
+ Parameters.register_domain ~name ~descr
let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction =
register_domain_option ~name ~experimental ~descr;
@@ -97,9 +97,9 @@ module Config = struct
(main, Domain_mode.Mode.all) :: mode
in
let add config (name, make) =
- let enabled = Value_parameters.Domains.mem name in
+ let enabled = Parameters.Domains.mem name in
try
- let mode = Value_parameters.DomainsFunction.find name in
+ let mode = Parameters.DomainsFunction.find name in
let mode = if enabled then add_main_mode mode else mode in
add (make (), Some mode) config
with Not_found ->
@@ -240,7 +240,7 @@ module Internal_Value = struct
end)
let void_value () =
- Value_parameters.fatal
+ Self.fatal
"Cannot register a value module from a Void structure."
let add_value_structure value internal =
@@ -352,7 +352,7 @@ let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc
module Store = struct
include Store
let register_global_state storage state =
- let no_results = Value_parameters.NoResultsDomains.mem dname in
+ let no_results = Parameters.NoResultsDomains.mem dname in
register_global_state (storage && not no_results) state
end
end in
@@ -386,7 +386,7 @@ let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc
let warn_experimental flag =
if flag.experimental then
- Value_parameters.(warning ~wkey:wkey_experimental
+ Self.(warning ~wkey:wkey_experimental
"The %s domain is experimental." flag.name)
let build_domain config abstract =
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index ada39c5e3fb927d537bc33de14cce090d91f33a9..4542b3f71043fe7379d47cfc53e545bfe0a861d8 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -209,7 +209,7 @@ let reset_analyzer () =
(* Builds the analyzer if needed, and run the analysis. *)
let force_compute () =
Ast.compute ();
- Value_parameters.configure_precision ();
+ Parameters.configure_precision ();
if not (Kernel.AuditCheck.is_empty ()) then
Eva_audit.check_configuration (Kernel.AuditCheck.get ());
let kf, lib_entry = Globals.entry_point () in
@@ -224,7 +224,7 @@ let is_computed = Db.Value.is_computed
let compute () =
(* Nothing to recompute when Value has already been computed. This boolean
is automatically cleared when an option of Value changes, because they
- are registered as dependencies on [Db.Value.self] in {!Value_parameters}.*)
+ are registered as dependencies on [Db.Value.self] in {!Parameters}.*)
if not (is_computed ()) then force_compute ()
(* Resets the Analyzer when the current project is changed. *)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 89f505305e48128fbed9ca567db7db6b36124c7b..30b31b9a20ac839f81baf14f926e3bfdd5e2658d 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -23,7 +23,7 @@
open Cil_types
open Eval
-let dkey = Value_parameters.register_category "callbacks"
+let dkey = Self.register_category "callbacks"
let floats_ok () =
let u = min_float /. 2. in
@@ -41,22 +41,22 @@ let options_ok () =
advanced parsing. Just make a query, as this will force the kernel to
parse them. *)
let check f = try ignore (f ()) with Not_found -> () in
- check Value_parameters.SplitReturnFunction.get;
- check Value_parameters.BuiltinsOverrides.get;
- check Value_parameters.SlevelFunction.get;
- check Value_parameters.EqualityCallFunction.get;
+ check Parameters.SplitReturnFunction.get;
+ check Parameters.BuiltinsOverrides.get;
+ check Parameters.SlevelFunction.get;
+ check Parameters.EqualityCallFunction.get;
let check_assigns kf =
if need_assigns kf then
- Value_parameters.error "@[no assigns@ specified@ for function '%a',@ for \
+ Self.error "@[no assigns@ specified@ for function '%a',@ for \
which@ a builtin@ or the specification@ will be used.@ \
Potential unsoundness.@]" Kernel_function.pretty kf
in
- Value_parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf);
- Value_parameters.UsePrototype.iter (fun kf -> check_assigns kf)
+ Parameters.BuiltinsOverrides.iter (fun (kf, _) -> check_assigns kf);
+ Parameters.UsePrototype.iter (fun kf -> check_assigns kf)
let plugins_ok () =
if not (Plugin.is_present "inout") then
- Value_parameters.warning
+ Self.warning
"The inout plugin is missing: some features are disabled, \
and the analysis may have degraded precision and performance."
@@ -66,15 +66,15 @@ let generate_specs () =
let aux kf =
if need_assigns kf then begin
let spec = Annotations.funspec ~populate:false kf in
- Value_parameters.warning "Generating potentially incorrect assigns \
+ Self.warning "Generating potentially incorrect assigns \
for function '%a' for which option %s is set"
- Kernel_function.pretty kf Value_parameters.UsePrototype.option_name;
+ Kernel_function.pretty kf Parameters.UsePrototype.option_name;
(* The function populate_spec may emit a warning. Position a loc. *)
Cil.CurrentLoc.set (Kernel_function.get_location kf);
ignore (!Annotations.populate_spec_ref kf spec)
end
in
- Value_parameters.UsePrototype.iter aux
+ Parameters.UsePrototype.iter aux
let pre_analysis () =
floats_ok ();
@@ -94,7 +94,7 @@ let pre_analysis () =
let post_analysis_cleanup ~aborted =
Value_util.clear_call_stack ();
(* Precompute consolidated states if required *)
- if Value_parameters.JoinResults.get () then
+ if Parameters.JoinResults.get () then
Db.Value.Table_By_Callstack.iter
(fun s _ -> ignore (Db.Value.get_stmt_state s));
if not aborted then
@@ -118,14 +118,14 @@ let post_analysis () =
Eva_dynamic.RteGen.mark_generated_rte ();
post_analysis_cleanup ~aborted:false;
(* Remove redundant alarms *)
- if Value_parameters.RmAssert.get () then Eva_dynamic.Scope.rm_asserts ()
+ if Parameters.RmAssert.get () then Eva_dynamic.Scope.rm_asserts ()
(* Registers signal handlers for SIGUSR1 and SIGINT to cleanly abort the Eva
analysis. Returns a function that restores previous signal behaviors after
the analysis. *)
let register_signal_handler () =
let warn () =
- Value_parameters.warning ~once:true "Stopping analysis at user request@."
+ Self.warning ~once:true "Stopping analysis at user request@."
in
let stop _ = warn (); Iterator.signal_abort () in
let interrupt _ = warn (); raise Sys.Break in
@@ -175,22 +175,22 @@ module Make (Abstract: Abstractions.Eva) = struct
let kf = call.kf in
Value_results.mark_kf_as_called kf;
let global = match call_kinstr with Kglobal -> true | _ -> false in
- let pp = not global && Value_parameters.ValShowProgress.get () in
+ let pp = not global && Parameters.ValShowProgress.get () in
let call_stack = Value_util.call_stack () in
if pp then
- Value_parameters.feedback
+ Self.feedback
"@[computing for function %a.@\nCalled from %a.@]"
Value_types.Callstack.pretty_short call_stack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc call_kinstr);
let use_spec =
match recursion with
- | Some { depth } when depth >= Value_parameters.RecursiveUnroll.get () ->
+ | Some { depth } when depth >= Parameters.RecursiveUnroll.get () ->
`Spec (Recursion.get_spec call_kinstr kf)
| _ ->
match kf.fundec with
| Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)
| Definition (def, _) ->
- if Kernel_function.Set.mem kf (Value_parameters.UsePrototype.get ())
+ if Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
then `Spec (Annotations.funspec kf)
else `Def def
in
@@ -199,9 +199,9 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Spec spec ->
Db.Value.Call_Type_Value_Callbacks.apply
(`Spec spec, cvalue_state, call_stack);
- if Value_parameters.InterpreterMode.get ()
- then Value_parameters.abort "Library function call. Stopping.";
- Value_parameters.feedback ~once:true
+ if Parameters.InterpreterMode.get ()
+ then Self.abort "Library function call. Stopping.";
+ Self.feedback ~once:true
"@[using specification for function %a@]" Kernel_function.pretty kf;
let vi = Kernel_function.get_vi kf in
if Cil.is_in_libc vi.vattr then
@@ -215,7 +215,7 @@ module Make (Abstract: Abstractions.Eva) = struct
result
in
if pp then
- Value_parameters.feedback
+ Self.feedback
"Done for function %a" Kernel_function.pretty kf;
Transfer.{ states = resulting_states; cacheable; builtin=false }
@@ -228,7 +228,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let default () =
compute_using_spec_or_body (Kstmt stmt) call recursion init_state
in
- if Value_parameters.MemExecAll.get () then
+ if Parameters.MemExecAll.get () then
let args =
List.map (fun {avalue} -> Eval.value_assigned avalue) call.arguments
in
@@ -257,10 +257,10 @@ module Make (Abstract: Abstractions.Eva) = struct
ignore (Logic.check_fct_preconditions
(Kstmt stmt) call.kf ab init_state);
end;
- if Value_parameters.ValShowProgress.get () then begin
- Value_parameters.feedback ~current:true
+ if Parameters.ValShowProgress.get () then begin
+ Self.feedback ~current:true
"Reusing old results for call to %a" Kernel_function.pretty call.kf;
- Value_parameters.debug ~dkey
+ Self.debug ~dkey
"calling Record_Value_New callbacks on saved previous result";
end;
let stack_with_call = Value_util.call_stack () in
@@ -295,9 +295,9 @@ module Make (Abstract: Abstractions.Eva) = struct
Value_results.mark_kf_as_called call.kf;
let kinstr = Kstmt stmt in
let kf_name = Kernel_function.get_name call.kf in
- if Value_parameters.ValShowProgress.get ()
+ if Parameters.ValShowProgress.get ()
then
- Value_parameters.feedback ~current:true "Call to builtin %s%s"
+ Self.feedback ~current:true "Call to builtin %s%s"
name (if kf_name = name then "" else " for function " ^ kf_name);
(* Do not track garbled mixes created when interpreting the specification,
as the result of the cvalue builtin will overwrite them. *)
@@ -355,7 +355,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let final_states = List.map snd (final_result.Transfer.states) in
let final_state = PowersetDomain.(final_states |> of_list |> join) in
Value_util.pop_call_stack ();
- Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
+ Self.feedback "done for function %a" Kernel_function.pretty kf;
Abstract.Dom.Store.mark_as_computed ();
post_analysis ();
Abstract.Dom.post_analysis final_state;
@@ -370,7 +370,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_from_entry_point kf ~lib_entry =
pre_analysis ();
- Value_parameters.feedback "Analyzing a%scomplete application starting at %a"
+ Self.feedback "Analyzing a%scomplete application starting at %a"
(if lib_entry then "n in" else " ")
Kernel_function.pretty kf;
let initial_state =
@@ -381,7 +381,7 @@ module Make (Abstract: Abstractions.Eva) = struct
match initial_state with
| `Bottom ->
Abstract.Dom.Store.mark_as_computed ();
- Value_parameters.result "Eva not started because globals \
+ Self.result "Eva not started because globals \
initialization is not computable.";
Eval_annots.mark_invalid_initializers ()
| `Value init_state ->
@@ -389,7 +389,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_from_init_state kf init_state =
pre_analysis ();
- let b = Value_parameters.ResultsAll.get () in
+ let b = Parameters.ResultsAll.get () in
Abstract.Dom.Store.register_global_state b (`Value init_state);
compute kf init_state
end
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index c194ece602cccce7dd801b1e183b30b32cb8c70f..58ba02483a7986b94991e8de5ef7a0126d40f992 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -119,8 +119,8 @@ let extern_report = { fuel = Infty; reduction = Neither; volatile = false }
let dummy_report = { fuel = Loop; reduction = Neither; volatile = false }
let no_fuel = -1
-let root_fuel () = Value_parameters.OracleDepth.get ()
-let backward_fuel () = Value_parameters.ReductionDepth.get ()
+let root_fuel () = Parameters.OracleDepth.get ()
+let backward_fuel () = Parameters.ReductionDepth.get ()
let already_precise_loc_report ~for_writing ~reduction loc_report =
(not for_writing || loc_report.for_writing)
@@ -137,7 +137,7 @@ let may_be_reduced_lval (host, offset) = match host with
| Mem _ -> true
let warn_pointer_comparison typ =
- match Value_parameters.WarnPointerComparison.get () with
+ match Parameters.WarnPointerComparison.get () with
| "none" -> false
| "all" -> true
| "pointer" -> Cil.isPointerType (Cil.unrollType typ)
@@ -145,7 +145,7 @@ let warn_pointer_comparison typ =
let propagate_all_pointer_comparison typ =
not (Cil.isPointerType typ)
- || Value_parameters.UndefinedPointerComparisonPropagateAll.get ()
+ || Parameters.UndefinedPointerComparisonPropagateAll.get ()
let comparison_kind = function
| Eq | Ne -> Some Abstract_value.Equality
@@ -455,7 +455,7 @@ module Make
else
let v = Value.rewrap_integer range value in
if range.Eval_typ.i_signed && not (Value.equal value v)
- then Value_parameters.warning ~wkey:Value_parameters.wkey_signed_overflow
+ then Self.warning ~wkey:Self.wkey_signed_overflow
~current:true ~once:true "2's complement assumed for overflow";
return v
@@ -575,7 +575,7 @@ module Make
| Shiftlt ->
let warn_negative = Kernel.LeftShiftNegative.get () in
reduce_shift ~warn_negative typ arg1 arg2
- | MinusPP when Value_parameters.WarnPointerSubstraction.get () ->
+ | MinusPP when Parameters.WarnPointerSubstraction.get () ->
let kind = Abstract_value.Subtraction in
let truth = Value.assume_comparable kind v1 v2 in
let alarm () = Alarms.Differing_blocks (e1, e2) in
@@ -612,9 +612,9 @@ module Make
else
let zero_or_one = Value.(join zero one) in
if Cil.isPointerType typ then
- Value_parameters.result
+ Self.result
~current:true ~once:true
- ~dkey:Value_parameters.dkey_pointer_comparison
+ ~dkey:Self.dkey_pointer_comparison
"evaluating condition to {0; 1} instead of %a because of UPCPA"
(Bottom.pretty pretty_zero_or_one) result;
`Value zero_or_one
@@ -695,7 +695,7 @@ module Make
in
if warn ()
then cast_integer overflow_kind expr ~src ~dst value
- else if dst.i_signed && Value_parameters.WarnSignedConvertedDowncast.get ()
+ else if dst.i_signed && Parameters.WarnSignedConvertedDowncast.get ()
then relaxed_signed_downcast expr ~src ~dst value
else return (Value.rewrap_integer dst value)
@@ -1034,7 +1034,7 @@ module Make
| Index (index_expr, remaining) ->
let typ_pointed, array_size = match Cil.unrollType typ with
| TArray (t, size, _) -> t, size
- | t -> Value_parameters.fatal ~current:true
+ | t -> Self.fatal ~current:true
"Got type '%a'" Printer.pp_typ t
in
eval_offset context ~reduce_valid_index typ_pointed remaining >>=
@@ -1144,7 +1144,7 @@ module Make
-eva-subdivide-non-linear. *)
let subdivision =
match subdivnb with
- | None -> Value_parameters.LinearLevel.get ()
+ | None -> Parameters.LinearLevel.get ()
| Some n -> n
in
let subdivided = false in
@@ -1618,16 +1618,16 @@ module Make
(* Aborts the analysis when a function pointer is completely imprecise. *)
let top_function_pointer funcexp =
- if not (Value_parameters.Domains.mem "cvalue") then
- Value_parameters.abort ~current:true
+ if not (Parameters.Domains.mem "cvalue") then
+ Self.abort ~current:true
"Calls through function pointers are not supported without the cvalue \
domain.";
if Mark_noresults.no_memoization_enabled () then
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"Function pointer evaluates to anything. Try deactivating \
option(s) -eva-no-results and -eva-no-results-function."
else
- Value_parameters.fatal ~current:true
+ Self.fatal ~current:true
"Function pointer evaluates to anything. function %a"
Printer.pp_exp funcexp
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index fd50fbc2765a12ec632190cd693e342373e59021..98c0b4c7377844058bbe7d355b2969a804f194e4 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -49,7 +49,7 @@ let padding_initialization ~local : padding_initialization =
if Kernel.InitializedPaddingLocals.get ()
then `Initialized else `Uninitialized
else
- match Value_parameters.InitializationPaddingGlobals.get () with
+ match Parameters.InitializationPaddingGlobals.get () with
| "yes" -> `Initialized
| "maybe" -> `MaybeInitialized
| "no" -> `Uninitialized
@@ -62,8 +62,8 @@ let warn_unknown_size vi =
false
with Cil.SizeOfError (s, t)->
let pp fmt v = Format.fprintf fmt "variable '%a'" Printer.pp_varinfo v in
- Value_parameters.warning ~once:true ~current:true
- ~wkey:Value_parameters.wkey_unknown_size
+ Self.warning ~once:true ~current:true
+ ~wkey:Self.wkey_unknown_size
"@[during initialization@ of %a,@ size of@ type '%a'@ cannot be@ \
computed@ (%s)@]" pp vi Printer.pp_typ t s;
true
@@ -131,7 +131,7 @@ module Make
match Transfer.assign state kinstr lval expr with
| `Bottom ->
if kinstr = Kglobal then
- Value_parameters.warning ~once:true ~source:(fst expr.eloc)
+ Self.warning ~once:true ~source:(fst expr.eloc)
"evaluation of initializer '%a' failed@." Printer.pp_exp expr;
raise Initialization_failed
| `Value v -> v
@@ -260,9 +260,9 @@ module Make
| Declaration (_, _, None, _) -> state
| Declaration (_, _, Some l, _)
| Definition ({ sformals = l }, _) ->
- if l <> [] && Value_parameters.InterpreterMode.get ()
+ if l <> [] && Parameters.InterpreterMode.get ()
then
- Value_parameters.abort "Entry point %a has arguments"
+ Self.abort "Entry point %a has arguments"
Kernel_function.pretty kf
else
let var_kind = Abstract_domain.Formal kf in
@@ -273,7 +273,7 @@ module Make
bind them in [state] *)
let add_supplied_main_formals kf actuals state =
match Domain.get_cvalue with
- | None -> Value_parameters.abort "Function Db.Value.fun_set_args cannot be \
+ | None -> Self.abort "Function Db.Value.fun_set_args cannot be \
used without the Cvalue domain"
| Some get_cvalue ->
let formals = Kernel_function.get_formals kf in
@@ -319,7 +319,7 @@ module Make
(* Compute the initial state with all global variable initialized. *)
let compute_global_state ~lib_entry () =
- Value_parameters.debug ~level:2 "Computing globals values";
+ Self.debug ~level:2 "Computing globals values";
let state = Domain.empty () in
let initialize = initialize_global_variable ~lib_entry in
try `Value (Globals.Vars.fold_in_file_order initialize state)
@@ -334,7 +334,7 @@ module Make
Ast.self ::
List.map
(fun p -> State.get p.Typed_parameter.name)
- Value_parameters.parameters_correctness
+ Parameters.parameters_correctness
module InitialState =
State_builder.Option_ref
@@ -379,7 +379,7 @@ module Make
then cvalue_state
else Cvalue.Model.filter_base print_base cvalue_state
in
- Value_parameters.printf ~dkey:Value_parameters.dkey_initial_state
+ Self.printf ~dkey:Self.dkey_initial_state
~header:(fun fmt -> Format.pp_print_string fmt
"Values of globals at initialization")
"@[ %a@]" Cvalue.Model.pretty cvalue_state
@@ -388,17 +388,17 @@ module Make
let init_state =
if Db.Value.globals_use_supplied_state ()
then begin
- Value_parameters.feedback "Initial state supplied by user";
+ Self.feedback "Initial state supplied by user";
supplied_state ()
end
else begin
- Value_parameters.feedback "Computing initial state";
+ Self.feedback "Computing initial state";
let state = global_state ~lib_entry in
- Value_parameters.feedback "Initial state computed";
+ Self.feedback "Initial state computed";
state
end
in
- let b = Value_parameters.ResultsAll.get () in
+ let b = Parameters.ResultsAll.get () in
Domain.Store.register_global_state b init_state;
print_initial_cvalue_state init_state;
init_state >>-: add_main_formals kf
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 773be0b00ab90f64fae7ca4f1b72b32c17e62b67..7e5856b22451e42bfcc4257f3140d08070313cc9 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -33,8 +33,8 @@ let check_signals, signal_abort =
end),
(fun () -> signal_emitted := true)
-let dkey = Value_parameters.dkey_iterator
-let dkey_callbacks = Value_parameters.dkey_callbacks
+let dkey = Self.dkey_iterator
+let dkey_callbacks = Self.dkey_callbacks
let blocks_share_locals b1 b2 =
match b1.blocals, b2.blocals with
@@ -74,17 +74,17 @@ module Make_Dataflow
type descending_strategy = NoIteration | FullIteration | ExitIteration
let descending_iteration : descending_strategy =
- match Value_parameters.DescendingIteration.get () with
+ match Parameters.DescendingIteration.get () with
| "no" -> NoIteration
| "exits" -> ExitIteration
| "full" -> FullIteration
| _ -> assert false
let hierachical_convergence : bool =
- Value_parameters.HierarchicalConvergence.get ()
+ Parameters.HierarchicalConvergence.get ()
let interpreter_mode =
- Value_parameters.InterpreterMode.get ()
+ Parameters.InterpreterMode.get ()
(* Ideally, the slevel parameter should not be used anymore in this file
but it is still required for logic interpretation *)
@@ -527,7 +527,7 @@ module Make_Dataflow
| [b,f,succ] -> (* One successor - continue simulation *)
simulate succ (b,f)
| _ -> (* Several successors - failure *)
- Value_parameters.abort "Do not know which branch to take. Stopping."
+ Self.abort "Do not know which branch to take. Stopping."
let reset_component (vertex_list : vertex list) : unit =
let reset_edge (_,e,_) =
@@ -560,7 +560,7 @@ module Make_Dataflow
while
not (process_vertex ~widening:true v) || !iteration_count = 0
do
- Value_parameters.debug ~dkey "iteration %d" !iteration_count;
+ Self.debug ~dkey "iteration %d" !iteration_count;
iterate_list w;
incr iteration_count;
done;
@@ -568,11 +568,11 @@ module Make_Dataflow
let l = match descending_iteration with
| NoIteration -> []
| ExitIteration ->
- Value_parameters.debug ~dkey
+ Self.debug ~dkey
"propagating descending values through exit paths";
Wto.flatten (exit_strategy graph component)
| FullIteration ->
- Value_parameters.debug ~dkey
+ Self.debug ~dkey
"propagating descending values through the loop";
v :: Wto.flatten w
in
@@ -708,26 +708,26 @@ module Make_Dataflow
end;
if not (Db.Value.Record_Value_Superposition_Callbacks.is_empty ())
then begin
- if Value_parameters.ValShowProgress.get () then
- Value_parameters.debug ~dkey:dkey_callbacks
+ if Parameters.ValShowProgress.get () then
+ Self.debug ~dkey:dkey_callbacks
"now calling Record_Value_Superposition callbacks";
Db.Value.Record_Value_Superposition_Callbacks.apply
(callstack, unmerged_pre_cvalues);
end;
if not (Db.Value.Record_Value_Callbacks.is_empty ())
then begin
- if Value_parameters.ValShowProgress.get () then
- Value_parameters.debug ~dkey:dkey_callbacks
+ if Parameters.ValShowProgress.get () then
+ Self.debug ~dkey:dkey_callbacks
"now calling Record_Value callbacks";
Db.Value.Record_Value_Callbacks.apply
(callstack, merged_pre_cvalues)
end;
if not (Db.Value.Record_Value_Callbacks_New.is_empty ())
then begin
- if Value_parameters.ValShowProgress.get () then
- Value_parameters.debug ~dkey:dkey_callbacks
+ if Parameters.ValShowProgress.get () then
+ Self.debug ~dkey:dkey_callbacks
"now calling Record_Value_New callbacks";
- if Value_parameters.MemExecAll.get () then
+ if Parameters.MemExecAll.get () then
Db.Value.Record_Value_Callbacks_New.apply
(callstack,
Value_types.NormalStore ((merged_pre_cvalues, merged_post_cvalues),
@@ -739,8 +739,8 @@ module Make_Dataflow
end;
if not (Db.Value.Record_Value_After_Callbacks.is_empty ())
then begin
- if Value_parameters.ValShowProgress.get () then
- Value_parameters.debug ~dkey:dkey_callbacks
+ if Parameters.ValShowProgress.get () then
+ Self.debug ~dkey:dkey_callbacks
"now calling Record_After_Value callbacks";
Db.Value.Record_Value_After_Callbacks.apply
(callstack, merged_post_cvalues);
@@ -774,8 +774,8 @@ module Computer
in
let compute () =
let results = Dataflow.compute () in
- if Value_parameters.ValShowProgress.get () then
- Value_parameters.feedback "Recording results for %a"
+ if Parameters.ValShowProgress.get () then
+ Self.feedback "Recording results for %a"
Kernel_function.pretty kf;
Dataflow.merge_results ();
let f = Kernel_function.get_definition kf in
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 71c6807a8fec3367044cdfc1717b4e4722b2629f..69c13c26cfc1ea57cc91846c5fc8d4c646c28884 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -47,7 +47,7 @@ let mark_unknown_requires kinstr kf funspec =
let get_spec kinstr kf =
let funspec = Annotations.funspec ~populate:false kf in
if Cil.is_empty_funspec funspec then begin
- Value_parameters.error ~current:true
+ Self.error ~current:true
"@[Recursive call to %a@ without a specification.@ \
Generating probably incomplete assigns to interpret the call.@ \
Try to increase@ the %s parameter@ \
@@ -56,7 +56,7 @@ let get_spec kinstr kf =
FRAMAC_SHARE/analysis-scripts/make_wrapper.py
*)
Kernel_function.pretty kf
- Value_parameters.RecursiveUnroll.name
+ Parameters.RecursiveUnroll.name
Kernel_function.pretty kf
Value_util.pp_callstack;
Cil.CurrentLoc.set (Kernel_function.get_location kf);
@@ -64,9 +64,9 @@ let get_spec kinstr kf =
Annotations.funspec kf
end
else
- let depth = Value_parameters.RecursiveUnroll.get () in
+ let depth = Parameters.RecursiveUnroll.get () in
let () =
- Value_parameters.warning ~once:true ~current:true
+ Self.warning ~once:true ~current:true
"@[Using specification of function %a@ for recursive calls%s.@ \
Analysis of function %a@ is thus incomplete@ and its soundness@ \
relies on the written specification.@]"
@@ -88,7 +88,7 @@ let _spec_for_recursive_call kf =
let assigns = Infer_annotations.assigns_from_prototype kf in
let bhv = Cil.mk_behavior ~assigns:(Writes assigns) () in
let spec = { (Cil.empty_funspec ()) with spec_behavior = [bhv] } in
- Value_parameters.error ~once:true
+ Self.error ~once:true
"@[recursive@ call@ on@ an unspecified@ \
function.@ Using@ potentially@ invalid@ inferred assigns '%t'@]"
(fun fmt -> match assigns with
@@ -154,8 +154,8 @@ let make_stack (kf, depth) =
let get_stack kf depth = VarStack.memo make_stack (kf, depth)
let make_recursion call depth =
- let dkey = Value_parameters.dkey_recursion in
- Value_parameters.feedback ~dkey ~once:true ~current:true
+ let dkey = Self.dkey_recursion in
+ Self.feedback ~dkey ~once:true ~current:true
"@[detected recursive call@ of function %a.@]"
Kernel_function.pretty call.kf;
let substitution = get_stack call.kf depth in
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 61a0a65264687d9a08090f372bfa90331d179aaa..ac077da8bab2e217c5b40909fcf413af0b2c74fc 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -23,7 +23,7 @@
open Cil_types
open Eval
-let dkey = Value_parameters.register_category "nonlin"
+let dkey = Self.register_category "nonlin"
(* ----------------- Occurrences of lvalues in expressions ------------------ *)
@@ -179,7 +179,7 @@ let compute_non_linear expr =
let list = reverse_map map in
List.iter
(fun (e, lval) ->
- Value_parameters.result ~current:true ~once:true ~dkey
+ Self.result ~current:true ~once:true ~dkey
"non-linear '%a', lv '%a'" Printer.pp_exp e
(Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lval)
list;
@@ -773,7 +773,7 @@ module Make
(subdivnb * nb) / (Integer.to_int_exn (pow 2 (nb - 1)))
else subdivnb
in
- Value_parameters.result ~current:true ~once:true ~dkey
+ Self.result ~current:true ~once:true ~dkey
"subdividing on %a"
(Pretty_utils.pp_list ~sep:", " Printer.pp_lval) lvals;
let subdivide =
@@ -905,7 +905,7 @@ module Make
let v = get_cval value in
if positive
then Cvalue.V.contains_non_zero v
- else if Value_parameters.UndefinedPointerComparisonPropagateAll.get ()
+ else if Parameters.UndefinedPointerComparisonPropagateAll.get ()
then Cvalue.V.contains_zero v
else Cvalue.V.is_included Cvalue.V.singleton_zero v
in
@@ -943,7 +943,7 @@ module Make
inoperative. Otherwise, it calls reduce_by_cond_enumerate with the
value accessor for the cvalue component. *)
let reduce_by_enumeration context valuation expr positive =
- if activated && Value_parameters.EnumerateCond.get ()
+ if activated && Parameters.EnumerateCond.get ()
then
get_influential_exprs valuation expr >>- fun split_on ->
reduce_by_cond_enumerate context valuation expr positive split_on
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index 95f0220637e68f331ec05c47d4f26b7a1ddaf603..dc07aad5c0143bbe49a14bb01b919541679ca632 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -74,9 +74,9 @@ let emit_status ppt status =
(* Display the message as result/warning depending on [status] *)
let msg_status status ?current ?once ?source fmt =
if status = Alarmset.True then
- if Value_parameters.ValShowProgress.get ()
- then Value_parameters.result ?current ?once ?source fmt
- else Value_parameters.result ?current ?once ?source ~level:2 fmt
+ if Parameters.ValShowProgress.get ()
+ then Self.result ?current ?once ?source fmt
+ else Self.result ?current ?once ?source ~level:2 fmt
else
Value_util.alarm_report ?current ?once ?source fmt
@@ -236,7 +236,7 @@ let process_inactive_behavior kf call_ki behavior =
end
) behavior.b_requires;
if !emitted then
- Value_parameters.result ~once:true ~current:true ~level:2
+ Self.result ~once:true ~current:true ~level:2
"%a: assumes got status invalid; behavior not evaluated.%t"
(pp_header kf) behavior Value_util.pp_callstack
@@ -258,7 +258,7 @@ let process_inactive_postconds kf inactive_bhvs =
end
) b.b_post_cond;
if !emitted then
- Value_parameters.result ~once:true ~current:true ~level:2
+ Self.result ~once:true ~current:true ~level:2
"%a: requires got status invalid; postconditions not evaluated.%t"
(pp_header kf) b Value_util.pp_callstack;
) inactive_bhvs
@@ -421,7 +421,7 @@ module Make
| Postcondition (PostLeaf | PostUseSpec) -> true
| _ -> false)
&& pr.pred_content <> Pfalse then
- Value_parameters.warning ~once:true ~source
+ Self.warning ~once:true ~source
"@[%a:@ this postcondition@ evaluates to@ false@ in this@ context.\
@ If it is valid,@ either@ a precondition@ was not@ verified@ \
for this@ call%t,@ or some assigns/from@ clauses@ are \
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 6c953deb3d14074c32383002bb96566a30f65cdf..92ece96f4d1c52df7816f354f6b4491e79fb3ed8 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -51,7 +51,7 @@ let warn_empty_from list =
| [] -> ()
| (out, _) :: _ ->
let source = fst out.it_content.term_loc in
- Value_parameters.warning ~source ~once:true
+ Self.warning ~source ~once:true
"@[no \\from part@ for clause '%a'@]"
Printer.pp_assigns (Writes no_from)
@@ -124,14 +124,14 @@ let warn_on_missing_result_assigns kinstr kf spec =
if return_used && not (List.for_all assigns_result spec.spec_behavior)
then
let source = fst (Kernel_function.get_location kf) in
- Value_parameters.warning ~once:true ~source
+ Self.warning ~once:true ~source
"@[no 'assigns \\result@ \\from ...'@ clause@ specified for@ function %a@]"
Kernel_function.pretty kf
let reduce_to_valid_location kind term loc =
if Locations.(Location_Bits.(equal top loc.loc)) then
begin
- Value_parameters.error ~once:true ~current:true
+ Self.error ~once:true ~current:true
"@[Cannot handle@ %a,@ location is too imprecise@ (%a).@ \
Assuming it is not assigned,@ but be aware@ this is incorrect.@]"
pp_assign_clause (kind, term) Locations.pretty loc;
@@ -142,8 +142,8 @@ let reduce_to_valid_location kind term loc =
if Locations.is_bottom_loc valid then
begin
if kind = Assign && not (Locations.is_bottom_loc loc) then
- Value_parameters.warning ~current:true ~once:true
- ~wkey:Value_parameters.wkey_invalid_assigns
+ Self.warning ~current:true ~once:true
+ ~wkey:Self.wkey_invalid_assigns
"@[Completely invalid destination@ for %a.@ \
Ignoring.@]" pp_assign_clause (kind, term);
None
@@ -313,8 +313,8 @@ module Make
then
begin
ignore (Locations.Location_Bytes.track_garbled_mix cvalue);
- Value_parameters.warning ~current:true ~once:true
- ~wkey:Value_parameters.wkey_garbled_mix
+ Self.warning ~current:true ~once:true
+ ~wkey:Self.wkey_garbled_mix
"The specification of function %a has generated a garbled mix \
for %a."
Kernel_function.pretty kf pp_assign_clause (Assign, assign)
@@ -488,7 +488,7 @@ module Make
| _ ->
let vi = Kernel_function.get_vi kf in
if not (Cil.hasAttribute "FC_BUILTIN" vi.vattr) then
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"ignoring unsupported allocates clause"
) behaviors
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 19c6c9973d540c62f1f070dc7f40fa2be9929b18..005d88b1eb4070cfe89e734ab5448a07b160a9c4 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -65,7 +65,7 @@ let current_kf_inout = InOutCallback.get_option
(* Should we warn about indeterminate copies in the function [kf] ? *)
let warn_indeterminate kf =
- let params = Value_parameters.WarnCopyIndeterminate.get () in
+ let params = Parameters.WarnCopyIndeterminate.get () in
Kernel_function.Set.mem kf params
(* An assignment from a right scalar lvalue is interpreted as a copy when
@@ -91,7 +91,7 @@ let is_determinate kf =
let subdivide_stmt = Value_util.get_subdivision
let subdivide_kinstr = function
- | Kglobal -> Value_parameters.LinearLevel.get ()
+ | Kglobal -> Parameters.LinearLevel.get ()
| Kstmt stmt -> subdivide_stmt stmt
(* Used to disambiguate files for Frama_C_dump_each_file directives. *)
@@ -137,12 +137,12 @@ module Make (Abstract: Abstractions.Eva) = struct
let notify_unreachability fmt =
if Domain.log_category = Domain_product.product_category
then
- Value_parameters.feedback ~level:1 ~current:true ~once:true
+ Self.feedback ~level:1 ~current:true ~once:true
"The evaluation of %(%a%)@ led to bottom without alarms:@ at this point \
the product of states has no possible concretization.@."
fmt
else
- Value_parameters.warning ~current:true
+ Self.warning ~current:true
"The evaluation of %(%a%)@ led to bottom without alarms:@ at this point \
the abstract state has no possible concretization,@ which is probably \
a bug."
@@ -151,8 +151,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let report_unreachability state (result, alarms) fmt =
if result = `Bottom && Alarmset.is_empty alarms
then begin
- Value_parameters.debug ~current:true ~once:true ~level:1
- ~dkey:Value_parameters.dkey_incompatible_states
+ Self.debug ~current:true ~once:true ~level:1
+ ~dkey:Self.dkey_incompatible_states
"State without concretization: %a" Domain.pretty state;
notify_unreachability fmt
end
@@ -509,7 +509,7 @@ module Make (Abstract: Abstractions.Eva) = struct
>>= fun (valuation, loc, typ) ->
if Int_Base.is_top (Location.size loc)
then
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"Function argument %a has unknown size. Aborting"
Printer.pp_exp expr;
if determinate && Cil.isArithmeticOrPointerType (Cil.typeOfLval lv)
@@ -591,7 +591,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let print_state =
if Domain.log_category = Domain_product.product_category
then Domain.pretty
- else if Value_parameters.is_debug_key_enabled Domain.log_category
+ else if Self.is_debug_key_enabled Domain.log_category
then
fun fmt state ->
Format.fprintf fmt "# %s:@ @[<hv>%a@]@ " Domain.name Domain.pretty state
@@ -599,7 +599,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Frama_C_dump_each functions. *)
let dump_state name state =
- Value_parameters.result ~current:true
+ Self.result ~current:true
"%s:@\n@[<v>%a@]==END OF DUMP==%t"
name print_state state Value_util.pp_callstack
@@ -607,7 +607,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let show_expr =
if Domain.log_category = Domain_product.product_category
then Domain.show_expr
- else if Value_parameters.is_debug_key_enabled Domain.log_category
+ else if Self.is_debug_key_enabled Domain.log_category
then
fun valuation state fmt exp ->
Format.fprintf fmt "# %s: @[<hov>%a@]"
@@ -627,7 +627,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Format.fprintf fmt "%a : @[<h>%t@]" Printer.pp_exp expr pp
in
let pp = Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@ " ~suf:"@]" pretty in
- Value_parameters.result ~current:true
+ Self.result ~current:true
"@[<v>%s:@ %a@]%t"
name pp arguments Value_util.pp_callstack
@@ -672,7 +672,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Frama_C_show_each functions. *)
let show_each ~subdivnb name arguments state =
- Value_parameters.result ~current:true
+ Self.result ~current:true
"@[<hv>%s:@ %a@]%t"
name (pretty_arguments ~subdivnb state) arguments Value_util.pp_callstack
@@ -691,7 +691,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let ch = open_out file in
let fmt = Format.formatter_of_out_channel ch in
let l = fst (Cil.CurrentLoc.get ()) in
- Value_parameters.feedback ~current:true "Dumping state in file '%s'%t"
+ Self.feedback ~current:true "Dumping state in file '%s'%t"
file Value_util.pp_callstack;
Format.fprintf fmt "DUMPING STATE at file %a line %d@."
Datatype.Filepath.pretty l.Filepath.pos_path
@@ -705,7 +705,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let dump_state_file ~subdivnb name arguments state =
try dump_state_file_exc ~subdivnb name arguments state
with e ->
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"Error during, or invalid call to Frama_C_dump_each_file (%s). Ignoring"
(Printexc.to_string e)
diff --git a/src/plugins/value/gen-api.sh b/src/plugins/value/gen-api.sh
index 82ce513c3bd3a9c39edda6e380afd1dab059e8ca..fa37740dc392f86cc112c3dd5e09e4a9d7b49416 100755
--- a/src/plugins/value/gen-api.sh
+++ b/src/plugins/value/gen-api.sh
@@ -8,7 +8,7 @@ printf '(** Eva public API.
and memory locations of lvalues at each program point.
The following modules allow configuring the Eva analysis:
- - Value_parameters: change the configuration of the analysis.
+ - Parameters: change the configuration of the analysis.
- Eva_annotations: add local annotations to guide the analysis.
- Builtins: register ocaml builtins to be used by the cvalue domain
instead of analysing the body of some C functions.
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index e73612e700b95212a5ce4160d64fcef3cd14b9cc..750c7e92888f3106cb404ad8f37b3763024de25b 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -114,21 +114,21 @@ let value_panel pack (main_ui:main_ui) =
in
let box_1_1 = GPack.hbox ~packing:(w#attach ~left:1 ~top:1) () in
let precision_refresh =
- let tooltip = Value_parameters.Precision.parameter.Typed_parameter.help in
+ let tooltip = Parameters.Precision.parameter.Typed_parameter.help in
Gtk_helper.on_int ~lower:(-1) ~upper:11 ~tooltip
box_1_1 "precision (meta-option)"
- Value_parameters.Precision.get
- Value_parameters.Precision.set
+ Parameters.Precision.get
+ Parameters.Precision.set
in
let box_1_2 = GPack.hbox ~packing:(w#attach ~left:1 ~top:2) () in
let slevel_refresh =
let tooltip =
- Value_parameters.SemanticUnrollingLevel.parameter.Typed_parameter.help
+ Parameters.SemanticUnrollingLevel.parameter.Typed_parameter.help
in
Gtk_helper.on_int ~lower:0 ~upper:1000000 ~tooltip
box_1_2 "slevel"
- Value_parameters.SemanticUnrollingLevel.get
- Value_parameters.SemanticUnrollingLevel.set
+ Parameters.SemanticUnrollingLevel.get
+ Parameters.SemanticUnrollingLevel.set
in
let box_1_3 = GPack.hbox ~packing:(w#attach ~left:1 ~top:3) () in
let validator s =
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 68aed0aadab7bc2b5171980bd0962f7b4f3e8c94..0baae6b9a5fb373299b2f8ff66bb9e193ab85356 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -46,7 +46,7 @@ let code_annotation_loc ca stmt =
let mark_unreachable () =
let mark ppt =
if not (Property_status.automatically_computed ppt) then begin
- Value_parameters.debug "Marking property %a as dead"
+ Self.debug "Marking property %a as dead"
Description.pp_property ppt;
let emit =
Property_status.emit ~distinct:false Value_util.emitter ~hyps:[]
@@ -190,7 +190,7 @@ let mark_green_and_red () =
Property_status.emit ~distinct Value_util.emitter ~hyps:[] ip status;
let source = fst loc in
let text_ca = code_annotation_text ca in
- Value_parameters.result ~once:true ~source "%s%a got final status %s."
+ Self.result ~once:true ~source "%s%a got final status %s."
text_ca Description.pp_named p text_status;
in
begin
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index 966726399171fb0f62b0454284db9e9fd23211eb..17c7822a2d94e30d1659b7e5533dc23919fb59aa 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -49,7 +49,7 @@ let v_uninit_of_offsetmap ~typ offsm =
V_Offsetmap.find ~validity ~conflate_bottom:false ~offsets ~size offsm
let backward_comp_int_left positive comp l r =
- if (Value_parameters.UndefinedPointerComparisonPropagateAll.get())
+ if (Parameters.UndefinedPointerComparisonPropagateAll.get())
&& not (Cvalue_forward.are_comparable comp l r)
then l
else
@@ -167,7 +167,7 @@ let apply_on_all_locs f loc state =
| Int_Base.Top -> state
| Int_Base.Value _ as size ->
let loc = Locations.valid_part Locations.Read loc in
- let plevel = Value_parameters.ArrayPrecisionLevel.get () in
+ let plevel = Parameters.ArrayPrecisionLevel.get () in
let ilevel = Int_set.get_small_cardinal () in
let limit = max plevel ilevel in
let apply_f base ival state =
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index a75bfed0d139992f8f602c3218285215a1101720..34a39cd38c3a3ec19db78105c7802633ca1eaa45 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -108,14 +108,14 @@ let track_alarms b = function
let display_evaluation_error ~loc = function
| CAlarm -> ()
| pa ->
- Value_parameters.result ~source:(fst loc) ~once:true
+ Self.result ~source:(fst loc) ~once:true
"cannot evaluate ACSL term, %a" pretty_logic_evaluation_error pa
(* Warning mode use when performing _reductions_ in the logic ( ** not **
evaluation). "Logic alarms" are ignored, and the reduction proceeds as if
they had not occurred. *)
let alarm_reduce_mode () =
- if Value_parameters.ReduceOnLogicAlarms.get () then Ignore else Fail
+ if Parameters.ReduceOnLogicAlarms.get () then Ignore else Fail
let find_indeterminate ~alarm_mode state loc =
let is_invalid = not Locations.(is_valid Read loc) in
@@ -853,7 +853,7 @@ let eval_logic_memchr_off builtin env s c n =
- otherwise, allocation always succeeds. *)
let eval_is_allocable size =
let size_ok = Builtins_malloc.alloc_size_ok size in
- match size_ok, Value_parameters.AllocReturnsNull.get () with
+ match size_ok, Parameters.AllocReturnsNull.get () with
| Alarmset.False, _ -> False
| Alarmset.Unknown, _ | _, true -> Unknown
| Alarmset.True, false -> True
@@ -1118,7 +1118,7 @@ let rec eval_term ~alarm_mode env t =
| Cvalue.V.Not_based_on_null -> None, None
| LogicEvalError e ->
if e <> CAlarm then
- Value_parameters.result ~source:(fst t.term_loc) ~once:true
+ Self.result ~source:(fst t.term_loc) ~once:true
"@[<hov 0>Cannot evaluate@ range bound %a@ (%a). Approximating@]"
Printer.pp_term term pretty_logic_evaluation_error e;
None, None
@@ -1330,7 +1330,7 @@ let rec eval_term ~alarm_mode env t =
and eval_binop ~alarm_mode env op t1 t2 =
if not (isLogicNonCompositeType t1.term_type) then
- if Value_parameters.debug_atleast 1 then
+ if Self.debug_atleast 1 then
unsupported (Format.asprintf
"operation (%a) %a (%a) on non-supported type %a"
Printer.pp_term t1
@@ -1378,7 +1378,7 @@ and eval_tif : 'a. (alarm_mode:_ -> _ -> _ -> 'a eval_result) -> ('a -> 'a -> 'a
let vtrue = eval ~alarm_mode env ttrue in
let vfalse = eval ~alarm_mode env tfalse in
if not (same_etype vtrue.etype vfalse.etype) then
- Value_parameters.failure ~current:true
+ Self.failure ~current:true
"Incoherent types in conditional: %a vs. %a. \
Please report"
Printer.pp_typ vtrue.etype Printer.pp_typ vfalse.etype;
@@ -2629,9 +2629,9 @@ and eval_predicate env pred =
| "\\warning", _ -> begin
match args with
| [{ term_node = TConst(LStr(str))}] ->
- Value_parameters.warning "reached \\warning(\"%s\")" str; Unknown
+ Self.warning "reached \\warning(\"%s\")" str; Unknown
| _ ->
- Value_parameters.abort
+ Self.abort
"Wrong argument: \\warning expects a constant string"
end
| "\\subset", [argl;argr] ->
diff --git a/src/plugins/value/legacy/function_args.ml b/src/plugins/value/legacy/function_args.ml
index 316201b1fd52de26cabeddb68f86f98dab3bde25..ce7e0ffd46503fcc7c2a51009692a612832ae6ff 100644
--- a/src/plugins/value/legacy/function_args.ml
+++ b/src/plugins/value/legacy/function_args.ml
@@ -54,7 +54,7 @@ let compute_actual state e =
let o =
try offsetmap_of_lv state lv
with Abstract_interp.Error_Top ->
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"Function argument %a has unknown size. Aborting" Printer.pp_exp e;
in begin
match o with
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/parameters.ml
similarity index 95%
rename from src/plugins/value/value_parameters.ml
rename to src/plugins/value/parameters.ml
index 11f8cce3e58081ea89ad878f2ad8534a50e6507e..0b994b78bd745a3db7b42fabc53a6404cbaa39ea 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/parameters.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Self
+
(* Dependencies to kernel options *)
let kernel_parameters_correctness = [
Kernel.MainFunction.parameter;
@@ -61,57 +63,6 @@ let add_precision_dep p =
let () = List.iter add_correctness_dep kernel_parameters_correctness
-include Plugin.Register
- (struct
- let name = "Eva"
- let shortname = "eva"
- let help =
- "automatically computes variation domains for the variables of the program"
- end)
-
-let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ]
-let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ]
-
-(* Debug categories. *)
-let dkey_initial_state = register_category "initial-state"
-let dkey_final_states = register_category "final-states"
-let dkey_summary = register_category "summary"
-let dkey_pointer_comparison = register_category "pointer-comparison"
-let dkey_cvalue_domain = register_category "d-cvalue"
-let dkey_incompatible_states = register_category "incompatible-states"
-let dkey_iterator = register_category "iterator"
-let dkey_callbacks = register_category "callbacks"
-let dkey_widening = register_category "widening"
-let dkey_recursion = register_category "recursion"
-
-let () =
- let activate dkey = add_debug_keys dkey in
- List.iter activate
- [dkey_initial_state; dkey_final_states; dkey_summary; dkey_cvalue_domain;
- dkey_recursion; ]
-
-(* Warning categories. *)
-let wkey_alarm = register_warn_category "alarm"
-let wkey_locals_escaping = register_warn_category "locals-escaping"
-let wkey_garbled_mix = register_warn_category "garbled-mix"
-let () = set_warn_status wkey_garbled_mix Log.Winactive
-let wkey_builtins_missing_spec = register_warn_category "builtins:missing-spec"
-let wkey_builtins_override = register_warn_category "builtins:override"
-let wkey_libc_unsupported_spec = register_warn_category "libc:unsupported-spec"
-let wkey_loop_unroll_auto = register_warn_category "loop-unroll:auto"
-let () = set_warn_status wkey_loop_unroll_auto Log.Wfeedback
-let wkey_loop_unroll_partial = register_warn_category "loop-unroll:partial"
-let () = set_warn_status wkey_loop_unroll_partial Log.Wfeedback
-let wkey_missing_loop_unroll = register_warn_category "loop-unroll:missing"
-let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
-let wkey_missing_loop_unroll_for = register_warn_category "loop-unroll:missing:for"
-let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
-let wkey_signed_overflow = register_warn_category "signed-overflow"
-let wkey_invalid_assigns = register_warn_category "invalid-assigns"
-let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
-let wkey_experimental = register_warn_category "experimental"
-let wkey_unknown_size = register_warn_category "unknown-size"
-
module ForceValues =
WithOutput
(struct
@@ -848,7 +799,7 @@ module SplitReturn =
module SplitGlobalStrategy = State_builder.Ref (Split_strategy)
(struct
let default () = Split_strategy.NoSplit
- let name = "Value_parameters.SplitGlobalStrategy"
+ let name = "Parameters.SplitGlobalStrategy"
let dependencies = [SplitReturn.self]
end)
let () =
@@ -1440,11 +1391,3 @@ let parameters_correctness =
Typed_parameter.Set.elements !parameters_correctness
let parameters_tuning =
Typed_parameter.Set.elements !parameters_tuning
-
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/parameters.mli
similarity index 70%
rename from src/plugins/value/value_parameters.mli
rename to src/plugins/value/parameters.mli
index 14c4e47e61ae888414a7e61a743f6f1af796a0dc..795cc6ab00344c8cadda67ace9ea91b6d98ac22c 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/parameters.mli
@@ -20,8 +20,6 @@
(* *)
(**************************************************************************)
-include Plugin.General_services
-
module ForceValues: Parameter_sig.With_output
module EnumerateCond: Parameter_sig.Bool
@@ -150,80 +148,6 @@ val configure_precision: unit -> unit
val parameters_correctness: Typed_parameter.t list
val parameters_tuning: Typed_parameter.t list
-(** Debug categories responsible for printing initial and final states of Value.
- Enabled by default, but can be disabled via the command-line:
- -value-msg-key="-initial_state,-final_state" *)
-val dkey_initial_state : category
-val dkey_final_states : category
-val dkey_summary : category
-
-(** Warning category used when emitting an alarm in "warning" mode. *)
-val wkey_alarm: warn_category
-
-(** Warning category used for the warning "locals escaping scope". *)
-val wkey_locals_escaping: warn_category
-
-(** Warning category used to print garbled mix *)
-val wkey_garbled_mix: warn_category
-
-(** Warning category used for "cannot use builtin due to missing spec" *)
-val wkey_builtins_missing_spec: warn_category
-
-(** Warning category used for "definition overridden by builtin" *)
-val wkey_builtins_override: warn_category
-
-(** Warning category used for calls to libc functions whose specification
- is currently unsupported. *)
-val wkey_libc_unsupported_spec : warn_category
-
-(** Warning category used for "Automatic loop unrolling" *)
-val wkey_loop_unroll_auto : warn_category
-
-(** Warning category used for "loop not completely unrolled" *)
-val wkey_loop_unroll_partial : warn_category
-
-(** Warning category used to identify loops without unroll annotations *)
-val wkey_missing_loop_unroll : warn_category
-
-(** Warning category used to identify for loops without unroll annotations *)
-val wkey_missing_loop_unroll_for : warn_category
-
-(** Warning category for signed overflows *)
-val wkey_signed_overflow : warn_category
-
-(** Warning category for 'completely invalid' assigns clause *)
-val wkey_invalid_assigns : warn_category
-
-(** Warning category for experimental domains or features. *)
-val wkey_experimental : warn_category
-
-(** Warning category for 'size of type T cannot be computed'. *)
-val wkey_unknown_size : warn_category
-
-(** Debug category used to print information about invalid pointer comparisons*)
-val dkey_pointer_comparison: category
-
-(** Debug category used to print the cvalue domain on Frama_C_[dump|show]_each
- functions. *)
-val dkey_cvalue_domain: category
-
-(* Print non-bottom product of states with no concretization, revealed by
- an evaluation leading to bottom without alarms. *)
-val dkey_incompatible_states: category
-
-(** Debug category used to print information about the iteration *)
-val dkey_iterator : category
-
-(** Debug category used when using Eva callbacks when recording the results of
- a function analysis. *)
-val dkey_callbacks : category
-
-(** Debug category used to print the usage of widenings. *)
-val dkey_widening : category
-
-(** Debug category used to print messages about recursive calls. *)
-val dkey_recursion : category
-
(** Registers available cvalue builtins for the -eva-builtin option. *)
val register_builtin: string -> unit
@@ -245,9 +169,3 @@ val use_builtin: Cil_types.kernel_function -> string -> unit
value partitioning on the global variable [vi]. *)
val use_global_value_partitioning: Cil_types.varinfo -> unit
[@@@ api_end]
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/plugins/value/partitioning/partition.ml b/src/plugins/value/partitioning/partition.ml
index cf2fac0814ab6c8ed278aff661939b3ca4d0c0fd..db974e60a0c4aa9b96b3690a2f8b1ff15d5472bd 100644
--- a/src/plugins/value/partitioning/partition.ml
+++ b/src/plugins/value/partitioning/partition.ml
@@ -372,7 +372,7 @@ struct
let fail ~exp message =
let source = fst exp.Cil_types.eloc in
let warn_and_raise message =
- Value_parameters.warning ~source ~once:true "%s" message;
+ Self.warning ~source ~once:true "%s" message;
raise Operation_failed
in
Pretty_utils.ksfprintf warn_and_raise message
@@ -476,7 +476,7 @@ struct
let x = Abstract.Dom.evaluate_predicate env state' predicate in
if x == Unknown
then
- Value_parameters.warning ~source ~once:true
+ Self.warning ~source ~once:true
"failing to learn perfectly from split predicate";
if Abstract.Dom.equal state' state then raise Operation_failed;
let value = if positive then Integer.one else Integer.zero in
@@ -502,7 +502,7 @@ struct
if Cvalue.V.cardinal_zero_or_one (get value)
then Some (stamp, 0)
else begin
- Value_parameters.result ~once:true ~current:true
+ Self.result ~once:true ~current:true
"cannot properly split on \\result == %a"
Abstract_interp.Int.pretty i;
None
@@ -569,8 +569,8 @@ struct
| None -> min_unroll
| Some i ->
let source = fst (Cil_datatype.Stmt.loc stmt) in
- Value_parameters.warning ~once:true ~current:true ~source
- ~wkey:Value_parameters.wkey_loop_unroll_auto
+ Self.warning ~once:true ~current:true ~source
+ ~wkey:Self.wkey_loop_unroll_auto
"Automatic loop unrolling.";
i
with
@@ -590,8 +590,8 @@ struct
| (h, limit) :: tl ->
if h >= limit then begin
if limit > 0 then
- Value_parameters.warning ~once:true ~current:true
- ~wkey:Value_parameters.wkey_loop_unroll_partial
+ Self.warning ~once:true ~current:true
+ ~wkey:Self.wkey_loop_unroll_partial
"loop not completely unrolled";
k
end
diff --git a/src/plugins/value/partitioning/partitioning_parameters.ml b/src/plugins/value/partitioning/partitioning_parameters.ml
index 77aecd2890d236914afb00f77473f73f280a2f4e..1bb96c5efea6dbabf5f8a3ac9790d28d222df492 100644
--- a/src/plugins/value/partitioning/partitioning_parameters.ml
+++ b/src/plugins/value/partitioning/partitioning_parameters.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Value_parameters
+open Parameters
open Eva_annotations
open Cil_types
@@ -69,10 +69,10 @@ struct
| loop_kind :: _ ->
let wkey =
if loop_kind = "for"
- then Value_parameters.wkey_missing_loop_unroll_for
- else Value_parameters.wkey_missing_loop_unroll
+ then Self.wkey_missing_loop_unroll_for
+ else Self.wkey_missing_loop_unroll
in
- Value_parameters.warning
+ Self.warning
~wkey ~source:(fst (Cil_datatype.Stmt.loc stmt)) ~once:true
"%s loop without unroll annotation" loop_kind
@@ -142,8 +142,8 @@ struct
let call_return_policy =
Partition.{
- callee_splits = Value_parameters.InterproceduralSplits.get ();
- callee_history = Value_parameters.InterproceduralHistory.get ();
+ callee_splits = Parameters.InterproceduralSplits.get ();
+ callee_history = Parameters.InterproceduralHistory.get ();
caller_history = true;
history_size = history_size;
}
diff --git a/src/plugins/value/partitioning/per_stmt_slevel.ml b/src/plugins/value/partitioning/per_stmt_slevel.ml
index 8ee8d668fcd7656eb067d52483726c4cdf643214..4631d81e56bfdd5b4ff34f0659dbfdbfae1c9dfb 100644
--- a/src/plugins/value/partitioning/per_stmt_slevel.ml
+++ b/src/plugins/value/partitioning/per_stmt_slevel.ml
@@ -132,7 +132,7 @@ let compute kf =
then NoMerge
else Merge (fun s -> Cil_datatype.Stmt.Hashtbl.mem h_merge s))
with Stack.Empty ->
- Value_parameters.abort
+ Self.abort
"Incorrectly nested slevel directives in function %a"
Kernel_function.pretty kf
@@ -142,7 +142,7 @@ module ForKf = Kernel_function.Make_Table
(struct
let size = 17
let dependencies =
- [Ast.self; Value_parameters.SemanticUnrollingLevel.self;]
+ [Ast.self; Parameters.SemanticUnrollingLevel.self;]
let name = "Value.Local_slevel.ForKf"
end)
diff --git a/src/plugins/value/partitioning/split_return.ml b/src/plugins/value/partitioning/split_return.ml
index c705fb09d4c455f65a48b83a8388a0f1c2828136..fe4ee995d773c8e3bf51c28d2d70101680c6c161 100644
--- a/src/plugins/value/partitioning/split_return.ml
+++ b/src/plugins/value/partitioning/split_return.ml
@@ -258,8 +258,8 @@ let find_auto_strategy kf =
module KfStrategy = Kernel_function.Make_Table(Split_strategy)
(struct
let size = 17
- let dependencies = [Value_parameters.SplitReturnFunction.self;
- Value_parameters.SplitGlobalStrategy.self;
+ let dependencies = [Parameters.SplitReturnFunction.self;
+ Parameters.SplitGlobalStrategy.self;
AutoStrategy.self]
let name = "Value.Split_return.Kfstrategy"
end)
@@ -269,11 +269,11 @@ let kf_strategy =
KfStrategy.memo
(fun kf ->
try (* User strategies take precedence *)
- match Value_parameters.SplitReturnFunction.find kf with
+ match Parameters.SplitReturnFunction.find kf with
| Split_strategy.SplitAuto -> find_auto_strategy kf
| s -> s
with Not_found ->
- match Value_parameters.SplitGlobalStrategy.get () with
+ match Parameters.SplitGlobalStrategy.get () with
| Split_strategy.SplitAuto -> find_auto_strategy kf
| s -> s
)
@@ -297,16 +297,16 @@ let pretty_strategies fmt =
| Some SplitAuto -> pp_one "auto" (pp_kf kf) (kf_strategy kf)
| Some s -> pp_one "user" (pp_kf kf) s
in
- Value_parameters.SplitReturnFunction.iter pp_user;
- if not (Value_parameters.SplitReturnFunction.is_empty ()) &&
- match Value_parameters.SplitGlobalStrategy.get () with
+ Parameters.SplitReturnFunction.iter pp_user;
+ if not (Parameters.SplitReturnFunction.is_empty ()) &&
+ match Parameters.SplitGlobalStrategy.get () with
| Split_strategy.NoSplit | Split_strategy.SplitAuto -> false
| _ -> true
then Format.fprintf fmt "@[other functions:@]@ ";
- begin match Value_parameters.SplitGlobalStrategy.get () with
+ begin match Parameters.SplitGlobalStrategy.get () with
| SplitAuto ->
let pp_auto kf s =
- if not (Value_parameters.SplitReturnFunction.mem kf) then
+ if not (Parameters.SplitReturnFunction.mem kf) then
let s = SplitEqList (Datatype.Integer.Set.elements s) in
pp_one "auto" (pp_kf kf) s
in
@@ -317,10 +317,10 @@ let pretty_strategies fmt =
Format.fprintf fmt "@]"
let pretty_strategies () =
- if not (Value_parameters.SplitReturnFunction.is_empty ()) ||
- (Value_parameters.SplitGlobalStrategy.get () != Split_strategy.NoSplit)
+ if not (Parameters.SplitReturnFunction.is_empty ()) ||
+ (Parameters.SplitGlobalStrategy.get () != Split_strategy.NoSplit)
then
- Value_parameters.result "Splitting return states on:@.%t" pretty_strategies
+ Self.result "Splitting return states on:@.%t" pretty_strategies
(*
diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index 61f2b7a458ffc32bdefebcfae7d7048304662d08..c4a30b874ecaa99bd7dc1ee5ccbd1cb01b271c71 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -28,10 +28,10 @@ module Make
(Abstract: Abstractions.Eva)
(Kf : sig val kf: kernel_function end) =
struct
- module Parameters = Partitioning_parameters.Make (Kf)
+ module Partition_parameters = Partitioning_parameters.Make (Kf)
open Kf
- open Parameters
+ open Partition_parameters
module Domain = Abstract.Dom
@@ -217,13 +217,13 @@ struct
let transfer = Flow.transfer
let output_slevel : int -> unit =
- let slevel_display_step = Value_parameters.ShowSlevel.get () in
+ let slevel_display_step = Parameters.ShowSlevel.get () in
let max_displayed = ref 0 in
fun x ->
if x >= !max_displayed + slevel_display_step
then
let rounded = x / slevel_display_step * slevel_display_step in
- Value_parameters.feedback ~once:true ~current:true
+ Self.feedback ~once:true ~current:true
"Trace partitioning superposing up to %d states"
rounded;
max_displayed := rounded
@@ -231,7 +231,7 @@ struct
let partitioning_feedback dest flow stmt =
output_slevel dest.incoming_states;
(* Debug information. *)
- Value_parameters.debug ~dkey:Value_parameters.dkey_iterator ~current:true
+ Self.debug ~dkey:Self.dkey_iterator ~current:true
"reached statement %d with %d incoming states, %d to propagate"
stmt.sid dest.incoming_states (flow_size flow)
@@ -279,7 +279,7 @@ struct
else begin
(* Propagate the join of the two states *)
if is_loop_head then
- Value_parameters.feedback ~level:1 ~once:true ~current:true
+ Self.feedback ~level:1 ~once:true ~current:true
"starting to merge loop iterations";
Some (Domain.join previous_state current_state)
end
@@ -321,8 +321,8 @@ struct
Some curr
(* Apply widening *)
else begin
- Value_parameters.feedback ~level:1 ~once:true ~current:true
- ~dkey:Value_parameters.dkey_widening
+ Self.feedback ~level:1 ~once:true ~current:true
+ ~dkey:Self.dkey_widening
"applying a widening at this point";
(* We join the previous widening state with the previous iteration
state so as to allow the intermediate(s) iteration(s) (between
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 2db4de10b3a0bc336b41126a07a126c0e2a181ae..4d242ad2cdfa4295ea1f081b8f73cf72253850e9 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -27,11 +27,11 @@ let [@alert "-deprecated"] _self =
Db.register_compute "Value.compute" [ Db.Value.self ] Db.Value.compute
Analysis.compute
-let () = Value_parameters.ForceValues.set_output_dependencies [Db.Value.self]
+let () = Parameters.ForceValues.set_output_dependencies [Db.Value.self]
let main () =
(* Value computations *)
- if Value_parameters.ForceValues.get () then !Db.Value.compute ();
+ if Parameters.ForceValues.get () then !Db.Value.compute ();
if Db.Value.is_computed () then Red_statuses.report ()
let () = Db.Main.extend main
@@ -60,7 +60,7 @@ let assigns_inputs_to_zone state assigns =
acc
l
with Eval_terms.LogicEvalError e ->
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"Failed to interpret inputs in assigns clause '%a'%a"
Printer.pp_from asgn eval_error_reason e;
Zone.top
@@ -79,7 +79,7 @@ let assigns_outputs_aux ~eval ~bot ~top ~join state ~result assigns =
let z = eval env out in
join z acc
with Eval_terms.LogicEvalError e ->
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"Failed to interpret assigns clause '%a'%a"
Printer.pp_term out eval_error_reason e;
join top acc
@@ -133,7 +133,7 @@ let use_spec_instead_of_definition kf =
not (Kernel_function.is_definition kf) ||
Ast_info.is_frama_c_builtin (Kernel_function.get_name kf) ||
Builtins.is_builtin_overridden kf ||
- Kernel_function.Set.mem kf (Value_parameters.UsePrototype.get ())
+ Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
let eval_predicate ~pre ~here p =
let open Eval_terms in
diff --git a/src/plugins/value/self.ml b/src/plugins/value/self.ml
new file mode 100644
index 0000000000000000000000000000000000000000..69af425301a4a9e69349acf600b3ce8788f8a8bb
--- /dev/null
+++ b/src/plugins/value/self.ml
@@ -0,0 +1,72 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Plugin.Register
+ (struct
+ let name = "Eva"
+ let shortname = "eva"
+ let help =
+ "automatically computes variation domains for the variables of the program"
+ end)
+
+let () = Help.add_aliases ~visible:false [ "-value-h"; "-val-h" ]
+let () = add_plugin_output_aliases ~visible:false ~deprecated:true [ "value" ]
+
+(* Debug categories. *)
+let dkey_initial_state = register_category "initial-state"
+let dkey_final_states = register_category "final-states"
+let dkey_summary = register_category "summary"
+let dkey_pointer_comparison = register_category "pointer-comparison"
+let dkey_cvalue_domain = register_category "d-cvalue"
+let dkey_incompatible_states = register_category "incompatible-states"
+let dkey_iterator = register_category "iterator"
+let dkey_callbacks = register_category "callbacks"
+let dkey_widening = register_category "widening"
+let dkey_recursion = register_category "recursion"
+
+let () =
+ let activate dkey = add_debug_keys dkey in
+ List.iter activate
+ [dkey_initial_state; dkey_final_states; dkey_summary; dkey_cvalue_domain;
+ dkey_recursion; ]
+
+(* Warning categories. *)
+let wkey_alarm = register_warn_category "alarm"
+let wkey_locals_escaping = register_warn_category "locals-escaping"
+let wkey_garbled_mix = register_warn_category "garbled-mix"
+let () = set_warn_status wkey_garbled_mix Log.Winactive
+let wkey_builtins_missing_spec = register_warn_category "builtins:missing-spec"
+let wkey_builtins_override = register_warn_category "builtins:override"
+let wkey_libc_unsupported_spec = register_warn_category "libc:unsupported-spec"
+let wkey_loop_unroll_auto = register_warn_category "loop-unroll:auto"
+let () = set_warn_status wkey_loop_unroll_auto Log.Wfeedback
+let wkey_loop_unroll_partial = register_warn_category "loop-unroll:partial"
+let () = set_warn_status wkey_loop_unroll_partial Log.Wfeedback
+let wkey_missing_loop_unroll = register_warn_category "loop-unroll:missing"
+let () = set_warn_status wkey_missing_loop_unroll Log.Winactive
+let wkey_missing_loop_unroll_for = register_warn_category "loop-unroll:missing:for"
+let () = set_warn_status wkey_missing_loop_unroll_for Log.Winactive
+let wkey_signed_overflow = register_warn_category "signed-overflow"
+let wkey_invalid_assigns = register_warn_category "invalid-assigns"
+let () = set_warn_status wkey_invalid_assigns Log.Wfeedback
+let wkey_experimental = register_warn_category "experimental"
+let wkey_unknown_size = register_warn_category "unknown-size"
diff --git a/src/plugins/value/self.mli b/src/plugins/value/self.mli
new file mode 100644
index 0000000000000000000000000000000000000000..94cd9910a275e60fd0c2b491c18bd430399f69d3
--- /dev/null
+++ b/src/plugins/value/self.mli
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Plugin.General_services
+
+(** Debug categories responsible for printing initial and final states of Value.
+ Enabled by default, but can be disabled via the command-line:
+ -value-msg-key="-initial_state,-final_state" *)
+val dkey_initial_state : category
+val dkey_final_states : category
+val dkey_summary : category
+
+(** {2 Debug categories.} *)
+
+val dkey_pointer_comparison: category
+val dkey_cvalue_domain: category
+val dkey_incompatible_states: category
+val dkey_iterator : category
+val dkey_callbacks : category
+val dkey_widening : category
+val dkey_recursion : category
+
+(** {2 Warning categories.} *)
+
+val wkey_alarm: warn_category
+val wkey_locals_escaping: warn_category
+val wkey_garbled_mix: warn_category
+val wkey_builtins_missing_spec: warn_category
+val wkey_builtins_override: warn_category
+val wkey_libc_unsupported_spec : warn_category
+val wkey_loop_unroll_auto : warn_category
+val wkey_loop_unroll_partial : warn_category
+val wkey_missing_loop_unroll : warn_category
+val wkey_missing_loop_unroll_for : warn_category
+val wkey_signed_overflow : warn_category
+val wkey_invalid_assigns : warn_category
+val wkey_experimental : warn_category
+val wkey_unknown_size : warn_category
diff --git a/src/plugins/value/utils/eva_annotations.ml b/src/plugins/value/utils/eva_annotations.ml
index c493b1149b5ddee3685b55fed93b5f4a85c70e30..5cebf4346f30a9ab6aa24cbbe136cae21fddb70c 100644
--- a/src/plugins/value/utils/eva_annotations.ml
+++ b/src/plugins/value/utils/eva_annotations.ml
@@ -341,10 +341,10 @@ module Allocation = struct
let get stmt =
match get stmt with
- | [] -> Option.get (of_string (Value_parameters.AllocBuiltin.get ()))
+ | [] -> Option.get (of_string (Parameters.AllocBuiltin.get ()))
| [x] -> x
| x :: _ ->
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"Several eva_allocate annotations at the same statement; selecting %s\
and ignoring the others." (to_string x);
x
diff --git a/src/plugins/value/utils/eva_audit.ml b/src/plugins/value/utils/eva_audit.ml
index d47d4c37275a36fa11f8229b9ec2fb4a3708af40..d5dc4c7a1c7b98b964667bb3cf90472fcdeda6c1 100644
--- a/src/plugins/value/utils/eva_audit.ml
+++ b/src/plugins/value/utils/eva_audit.ml
@@ -26,7 +26,7 @@ let get_correctness_parameters () =
let value = Typed_parameter.get_value param in
(name, value)
in
- List.map get (Value_parameters.parameters_correctness)
+ List.map get (Parameters.parameters_correctness)
let parameters_of_json json =
try
@@ -45,8 +45,8 @@ let parameters_of_json json =
let print_correctness_parameters path =
let parameters = get_correctness_parameters () in
if Filepath.Normalized.is_special_stdout path then begin
- Value_parameters.feedback "Correctness parameters of the analysis:";
- let print (name, value) = Value_parameters.printf " %s: %s" name value in
+ Self.feedback "Correctness parameters of the analysis:";
+ let print (name, value) = Self.printf " %s: %s" name value in
List.iter print parameters
end else begin
let json = List.map (fun (name, value) -> name, `String value) parameters in
@@ -106,10 +106,10 @@ let print_warning_status path name (module Plugin: Log.Messages) =
let pp_categories =
Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string
in
- Value_parameters.feedback "Audit: %s warning categories:" name;
- Value_parameters.printf " Enabled: @[%a@]"
+ Self.feedback "Audit: %s warning categories:" name;
+ Self.printf " Enabled: @[%a@]"
pp_categories (List.map fst enabled);
- Value_parameters.printf " Disabled: @[%a@]"
+ Self.printf " Disabled: @[%a@]"
pp_categories (List.map fst disabled)
end
else begin
@@ -139,7 +139,7 @@ let check_configuration path =
let json = Json.from_file path in
check_correctness_parameters json;
check_warning_status json "Kernel" (module Kernel);
- check_warning_status json "Eva" (module Value_parameters)
+ check_warning_status json "Eva" (module Self)
with Yojson.Json_error msg ->
Kernel.abort "error reading JSON file %a: %s"
Filepath.Normalized.pretty path msg
@@ -148,9 +148,9 @@ let print_configuration path =
try
print_correctness_parameters path;
print_warning_status path "Kernel" (module Kernel);
- print_warning_status path "Eva" (module Value_parameters);
+ print_warning_status path "Eva" (module Self);
if not (Filepath.Normalized.is_special_stdout path) then
- Value_parameters.feedback "Audit: eva configuration written to: %a"
+ Self.feedback "Audit: eva configuration written to: %a"
Filepath.Normalized.pretty path;
with Json.CannotMerge _ ->
Kernel.failure "%s: error when writing json file %a."
diff --git a/src/plugins/value/utils/eva_dynamic.ml b/src/plugins/value/utils/eva_dynamic.ml
index b62a8ec73cb2f5f61f8db4a83e434ccfcbc2f15b..5be50585b9e36feed52b361391cf370aaf14a74c 100644
--- a/src/plugins/value/utils/eva_dynamic.ml
+++ b/src/plugins/value/utils/eva_dynamic.ml
@@ -43,7 +43,7 @@ module Scope = struct
let rm_asserts () =
let fallback () =
- Value_parameters.warning
+ Self.warning
"The scope plugin is missing: cannot remove redundant alarms."
in
let typ = Datatype.(func unit unit) in
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index 9d729c7e8eb674c3a03612de4ee59f89a84e3f77..4b6ddb5553fc66e35ccd94b2e7a49192999af032 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -47,7 +47,7 @@ let get_retres_vi = Retres.memo
let name = Format.asprintf "\\result<%a>" Kernel_function.pretty kf in
Some (Cil.makeVarinfo false false name typ)
with Cil.SizeOfError _ ->
- Value_parameters.abort ~current:true
+ Self.abort ~current:true
"function %a returns a value of unknown size. Aborting"
Kernel_function.pretty kf
)
@@ -62,7 +62,7 @@ let returned_value kf =
| TFloat (FDouble, _)
| TFloat (FLongDouble, _) -> Cvalue.V.top_float
| TBuiltin_va_list _ ->
- Value_parameters.error ~current:true ~once:true
+ Self.error ~current:true ~once:true
"functions returning variadic arguments must be stubbed%t"
Value_util.pp_callstack;
Cvalue.V.top_int
@@ -100,8 +100,8 @@ let unsupported_specs_tbl =
let warn_unsupported_spec name =
try
let header = Hashtbl.find unsupported_specs_tbl name in
- Value_parameters.warning ~once:true ~current:true
- ~wkey:Value_parameters.wkey_libc_unsupported_spec
+ Self.warning ~once:true ~current:true
+ ~wkey:Self.wkey_libc_unsupported_spec
"@[The specification of function '%s' is currently not supported by Eva.@ \
Consider adding '%a'@ to the analyzed source files.@]"
name Filepath.Normalized.pretty
diff --git a/src/plugins/value/utils/mark_noresults.ml b/src/plugins/value/utils/mark_noresults.ml
index 0c31fbf0eda5e2154995879b8f7f7e7d501c1741..913698fdaaf7d2ca309bc1b250134809630ba05a 100644
--- a/src/plugins/value/utils/mark_noresults.ml
+++ b/src/plugins/value/utils/mark_noresults.ml
@@ -21,19 +21,19 @@
(**************************************************************************)
let should_memorize_function f =
- Value_parameters.ResultsAll.get () &&
+ Parameters.ResultsAll.get () &&
not (Cil_datatype.Fundec.Set.mem
- f (Value_parameters.NoResultsFunctions.get ()))
+ f (Parameters.NoResultsFunctions.get ()))
let () = Db.Value.no_results :=
(fun fd -> not (should_memorize_function fd)
- || not (Value_parameters.Domains.mem "cvalue"))
+ || not (Parameters.Domains.mem "cvalue"))
(* Signal that some results are not stored. The gui, or some calls to
Db.Value, may fail ungracefully *)
let no_memoization_enabled () =
- not (Value_parameters.ResultsAll.get ()) ||
- not (Value_parameters.NoResultsFunctions.is_empty ())
+ not (Parameters.ResultsAll.get ()) ||
+ not (Parameters.NoResultsFunctions.is_empty ())
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index 42440721ae25d8f7b25c9e1809bc32bb6c808c6a..a326f184a2c517c19941b2d5c09896dd4d190e0c 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -194,7 +194,7 @@ 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 %a"
+ Self.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
@@ -209,4 +209,4 @@ let output file =
Format.fprintf fmt "@]%!"
let report () =
- Value_parameters.ReportRedStatuses.(if not (is_empty ()) then output (get ()))
+ Parameters.ReportRedStatuses.(if not (is_empty ()) then output (get ()))
diff --git a/src/plugins/value/utils/summary.ml b/src/plugins/value/utils/summary.ml
index 1429c0262b314bff082b941cf0e2fe9d495a1245..a56f47b4ec1983cac86380c565e0433e163a85af 100644
--- a/src/plugins/value/utils/summary.ml
+++ b/src/plugins/value/utils/summary.ml
@@ -427,6 +427,6 @@ let print_summary fmt =
Format.fprintf fmt "%s" bar
let print_summary () =
- let dkey = Value_parameters.dkey_summary in
+ let dkey = Self.dkey_summary in
let header fmt = Format.fprintf fmt " ====== ANALYSIS SUMMARY ======" in
- Value_parameters.printf ~header ~dkey ~level:1 " @[<v>%t@]" print_summary
+ Self.printf ~header ~dkey ~level:1 " @[<v>%t@]" print_summary
diff --git a/src/plugins/value/utils/unit_tests.ml b/src/plugins/value/utils/unit_tests.ml
index 50ef12be9835c4b409339706e9f370ed91d7a363..b7261099a512d7dc08cc405d807bae63d7d39416 100644
--- a/src/plugins/value/utils/unit_tests.ml
+++ b/src/plugins/value/utils/unit_tests.ml
@@ -28,7 +28,7 @@ let print = false
let report bug format =
if print || bug
- then Value_parameters.result ("%s" ^^ format) (if bug then "BUG " else "")
+ then Self.result ("%s" ^^ format) (if bug then "BUG " else "")
else Format.ifprintf Format.std_formatter format
@@ -128,7 +128,7 @@ end
(** Runs all tests. *)
let run () =
- Value_parameters.result "Runs unit tests: %s."
+ Self.result "Runs unit tests: %s."
(if print
then "all operations will be printed"
else "only faulty operations will be printed");
diff --git a/src/plugins/value/utils/value_perf.ml b/src/plugins/value/utils/value_perf.ml
index 5d1d845e294d1fcac34816b8f2821c8cf04ba20f..66f45a43f9c48b809c33365a6ed2bbc0e1b22f4f 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/value_perf.ml
@@ -271,7 +271,7 @@ and display_subtree fmt indentation subtree parent_duration curtime =
;;
let display fmt =
- if Value_parameters.ValShowPerf.get()
+ if Parameters.ValShowPerf.get()
then begin
Format.fprintf fmt "####### Value execution feedback #########\n";
let current_time = (Sys.time()) in
@@ -299,7 +299,7 @@ let caller_callee_callinfo = function
;;
let start_doing_perf callstack =
- if Value_parameters.ValShowPerf.get()
+ if Parameters.ValShowPerf.get()
then begin
let time = Sys.time() in
assert (callstack != []);
@@ -322,7 +322,7 @@ let start_doing_perf callstack =
;;
let stop_doing_perf callstack =
- if Value_parameters.ValShowPerf.get()
+ if Parameters.ValShowPerf.get()
then begin
let time = Sys.time() in
let kf = fst (List.hd callstack) in
@@ -389,15 +389,15 @@ let start_doing_flamegraph callstack =
| [] -> assert false
| [_] ->
(* Analysis of main *)
- if not (Value_parameters.ValPerfFlamegraphs.is_empty ()) then begin
- let file = Value_parameters.ValPerfFlamegraphs.get () in
+ if not (Parameters.ValPerfFlamegraphs.is_empty ()) then begin
+ let file = Parameters.ValPerfFlamegraphs.get () in
try
(* Flamegraphs must be computed. Set up the stack and the output file *)
let oc = open_out (file:>string) in
oc_flamegraph := Some oc;
stack_flamegraph := [ (Sys.time (), 0.) ]
with e ->
- Value_parameters.error "cannot open flamegraph file: %s"
+ Self.error "cannot open flamegraph file: %s"
(Printexc.to_string e);
oc_flamegraph := None (* to be on the safe side *)
end
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index cd0d402e1f9da9f64142f1ba106955cbc0b73b3c..a3c7470b3ef60d7ce16a48f7d4bc25e80365d021 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -47,7 +47,7 @@ let current_kf () =
let call_stack () = !call_stack
let pp_callstack fmt =
- if Value_parameters.PrintCallstacks.get () then
+ if Parameters.PrintCallstacks.get () then
Format.fprintf fmt "@ stack: %a"
Value_types.Callstack.pretty (call_stack())
;;
@@ -58,27 +58,27 @@ let emitter =
Emitter.create
"Eva"
[ Emitter.Property_status; Emitter.Alarm ]
- ~correctness:Value_parameters.parameters_correctness
- ~tuning:Value_parameters.parameters_tuning
+ ~correctness:Parameters.parameters_correctness
+ ~tuning:Parameters.parameters_tuning
let () = Db.Value.emitter := emitter
let get_slevel kf =
- try Value_parameters.SlevelFunction.find kf
- with Not_found -> Value_parameters.SemanticUnrollingLevel.get ()
+ try Parameters.SlevelFunction.find kf
+ with Not_found -> Parameters.SemanticUnrollingLevel.get ()
let get_subdivision_option stmt =
try
let kf = Kernel_function.find_englobing_kf stmt in
- Value_parameters.LinearLevelFunction.find kf
- with Not_found -> Value_parameters.LinearLevel.get ()
+ Parameters.LinearLevelFunction.find kf
+ with Not_found -> Parameters.LinearLevel.get ()
let get_subdivision stmt =
match Eva_annotations.get_subdivision_annot stmt with
| [] -> get_subdivision_option stmt
| [x] -> x
| x :: _ ->
- Value_parameters.warning ~current:true ~once:true
+ Self.warning ~current:true ~once:true
"Several subdivision annotations at the same statement; selecting %i\
and ignoring the others." x;
x
@@ -91,11 +91,11 @@ let pretty_current_cfunction_name fmt =
Kernel_function.pretty fmt (current_kf())
let warning_once_current fmt =
- Value_parameters.warning ~current:true ~once:true fmt
+ Self.warning ~current:true ~once:true fmt
(* Emit alarms in "non-warning" mode *)
let alarm_report ?current ?source ?emitwith ?echo ?once ?append =
- Value_parameters.warning ~wkey:Value_parameters.wkey_alarm
+ Self.warning ~wkey:Self.wkey_alarm
?current ?source ?emitwith ?echo ?once ?append
module DegenerationPoints =
@@ -112,7 +112,7 @@ let protect_only_once = ref true
let protect f ~cleanup =
let catch () = !protect_only_once && not (Kernel.SaveState.is_empty ()) in
let cleanup () =
- Value_parameters.feedback ~once:true "Clean up and save partial results.";
+ Self.feedback ~once:true "Clean up and save partial results.";
try cleanup ()
with e ->
protect_only_once := false;
@@ -201,7 +201,7 @@ let zero e =
let ik = Cil.(theMachine.upointKind) in
let zero = Cil.new_exp ~loc (Const (CInt64 (Integer.zero, ik, None))) in
Cil.mkCast ~force:true ~newt:typ zero
- | typ -> Value_parameters.fatal ~current:true "non-scalar type %a"
+ | typ -> Self.fatal ~current:true "non-scalar type %a"
Printer.pp_typ typ
let eq_with_zero positive e =
@@ -268,7 +268,7 @@ let dump_garbled_mix () =
let l = Cvalue.V.get_garbled_mix () in
if l <> [] then
let pp_one fmt v = Format.fprintf fmt "@[<hov 2>%a@]" Cvalue.V.pretty v in
- Value_parameters.warning ~wkey:Value_parameters.wkey_garbled_mix
+ Self.warning ~wkey:Self.wkey_garbled_mix
"Garbled mix generated during analysis:@.\
@[<v>%a@]"
(Pretty_utils.pp_list ~pre:"" ~suf:"" ~sep:"@ " pp_one) l
@@ -347,7 +347,7 @@ and height_offset = function
let skip_specifications kf =
- Value_parameters.SkipLibcSpecs.get () &&
+ Parameters.SkipLibcSpecs.get () &&
Kernel_function.is_definition kf &&
Cil.is_in_libc (Kernel_function.get_vi kf).vattr
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index c99393d8885d66b5e1e11023582e3b7b797f05c7..b784b933c600a19a959c61838a07c48e38b503fb 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -40,7 +40,7 @@ val pp_callstack : Format.formatter -> unit
(* TODO: Document the rest of this file. *)
val emitter : Emitter.t
-val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
+val get_slevel : Kernel_function.t -> Parameters.SlevelFunction.value
val get_subdivision: stmt -> int
val pretty_actuals :
Format.formatter -> (Cil_types.exp * Cvalue.V.t) list -> unit
@@ -48,7 +48,7 @@ val pretty_current_cfunction_name : Format.formatter -> unit
val warning_once_current : ('a, Format.formatter, unit) format -> 'a
(** Emit an alarm, either as warning or as a result, according to
- status associated to {!Value_parameters.wkey_alarm} *)
+ status associated to {!Self.wkey_alarm} *)
val alarm_report: 'a Log.pretty_printer
(** [protect f ~cleanup] runs [f]. On a user interruption or a Frama-C error,
diff --git a/src/plugins/value/utils/widen.ml b/src/plugins/value/utils/widen.ml
index b124349d7b634f4038e1d7da6f9c3ca623254e9f..05a9e0477af7e53e752b2c68e778a4d5b53bf4d4 100644
--- a/src/plugins/value/utils/widen.ml
+++ b/src/plugins/value/utils/widen.ml
@@ -98,7 +98,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
(* the annotation is empty or contains only variables *)
self#add_var_hints ~stmt var_hints
| (_lv, _lt) ->
- Value_parameters.warning ~once:true
+ Self.warning ~once:true
"could not interpret loop pragma relative to widening variables"
end
| Widen_hints l -> begin
@@ -124,7 +124,7 @@ class pragma_widen_visitor init_widen_hints init_enclosing_loops = object(self)
self#add_float_thresholds ~base float_thresholds;
) vars
| _ ->
- Value_parameters.warning ~once:true
+ Self.warning ~once:true
"could not interpret loop pragma relative to widening hint"
end
| _ -> ()
@@ -314,7 +314,7 @@ let base_of_static_hvars hvars =
| Widen_hints_ext.HintVar vi -> Some (Base.of_varinfo vi)
| Widen_hints_ext.HintMem (e, offset) ->
(* syntactic constraints prevent this from happening *)
- Value_parameters.fatal "unsupported lhost: %a" Printer.pp_lval (Mem e, offset)
+ Self.fatal "unsupported lhost: %a" Printer.pp_lval (Mem e, offset)
type threshold = Int_th of Integer.t | Real_th of logic_real
@@ -332,7 +332,7 @@ let threshold_of_threshold_term ht =
match constFoldTermToLogicReal ht.term_node with
| Some f -> Real_th f
| None ->
- Value_parameters.abort ~source:(fst ht.term_loc)
+ Self.abort ~source:(fst ht.term_loc)
"could not parse widening hint: %a@ \
If it contains variables, they must be global const integers."
Printer.pp_term ht
@@ -344,14 +344,14 @@ let thresholds_of_threshold_terms hts =
match threshold_of_threshold_term ht with
| Int_th i ->
if !has_float then
- Value_parameters.abort ~source:(fst ht.term_loc)
+ Self.abort ~source:(fst ht.term_loc)
"widening hint mixing integers and floats: %a"
Printer.pp_term ht;
has_int := true;
Ival.Widen_Hints.add i int_acc, float_acc
| Real_th f ->
if !has_int then
- Value_parameters.abort ~source:(fst ht.term_loc)
+ Self.abort ~source:(fst ht.term_loc)
"widening hint mixing integers and floats: %a"
Printer.pp_term ht;
has_float := true;
@@ -374,7 +374,7 @@ class hints_visitor init_widen_hints global = object(self)
let int_thresholds, float_thresholds =
thresholds_of_threshold_terms wh_terms
in
- Value_parameters.feedback ~source:(fst loc) ~dkey
+ Self.feedback ~source:(fst loc) ~dkey
"adding%s hint from annotation: %a, %t (for all statements)"
(if global then " global" else "")
(Pretty_utils.pp_opt ~none:(format_of_string "for all variables")
@@ -405,7 +405,7 @@ end
(* Precompute global widen hints, used for all functions *)
let compute_global_static_hints () =
- Value_parameters.debug ~dkey "computing global widen hints";
+ Self.debug ~dkey "computing global widen hints";
let global_widen_hints = ref (Global_Static_Hints.get ()) in
Globals.Functions.iter_on_fundecs (fun fd ->
let visitor = new hints_visitor global_widen_hints true in
@@ -508,7 +508,7 @@ let dynamic_bases_of_lval states e offset =
(* Find syntactically the dynamic hints on [stmt]. *)
let extract_dynamic_hints stmt =
let source = fst (Stmt.loc stmt) in
- Value_parameters.debug ~source ~dkey
+ Self.debug ~source ~dkey
"computing dynamic hints for statement %d" stmt.sid;
let wh = Widen_hints_ext.get_stmt_widen_hint_terms stmt in
let aux l (hlv, threshold_terms) =
@@ -577,7 +577,7 @@ let dynamic_widen_hints_hook (stmt, _callstack, states) =
else
let new_hints =
Base.Hptset.fold (fun base acc ->
- Value_parameters.debug ~source ~dkey
+ Self.debug ~source ~dkey
"adding new base due to dynamic widen hint: %a, %a%a"
Base.pretty base
Ival.Widen_Hints.pretty dhint.int_thresholds
diff --git a/src/plugins/value/utils/widen_hints_ext.ml b/src/plugins/value/utils/widen_hints_ext.ml
index f7e2aef59a10a8b4e7fbeb9e7e6525009917ee39..bd46d2b96f4b737b2398b144bed8804c9181ebc4 100644
--- a/src/plugins/value/utils/widen_hints_ext.ml
+++ b/src/plugins/value/utils/widen_hints_ext.ml
@@ -22,7 +22,7 @@
open Cil_types
-let dkey = Value_parameters.register_category "widen-hints"
+let dkey = Self.register_category "widen-hints"
let error ?msg loc typing_context =
typing_context.Logic_typing.error loc
@@ -126,12 +126,12 @@ let widen_hint_terms_of_terms terms =
in
Some (hint_lval, hint_thresholds)
| _ ->
- Value_parameters.debug ~source:(fst lval_term.term_loc) ~dkey
+ Self.debug ~source:(fst lval_term.term_loc) ~dkey
"invalid var_term: %a@." Printer.pp_term lval_term;
raise Invalid_hint
end
| _ ->
- Value_parameters.debug ~dkey "invalid terms: %a@."
+ Self.debug ~dkey "invalid terms: %a@."
(Pretty_utils.pp_list ~sep:", " Printer.pp_term) terms;
raise Invalid_hint
with
diff --git a/src/plugins/value/utils/widen_hints_ext.mli b/src/plugins/value/utils/widen_hints_ext.mli
index e17c19f6d0115b790c6d44f537670af206b4e0e1..c65b2be878da5f9638c8b33e16caaa8524048cab 100644
--- a/src/plugins/value/utils/widen_hints_ext.mli
+++ b/src/plugins/value/utils/widen_hints_ext.mli
@@ -24,7 +24,7 @@
open Cil_types
-val dkey: Value_parameters.category
+val dkey: Self.category
type hint_vars =
| HintAllVars (* "all" vars: static hint *)
diff --git a/src/plugins/value/values/cvalue_backward.ml b/src/plugins/value/values/cvalue_backward.ml
index 889c776877859e26044a9b2aa40ea1c4b7d479c8..0993a32bba3725c629cb9cd164c208142ef2f8d8 100644
--- a/src/plugins/value/values/cvalue_backward.ml
+++ b/src/plugins/value/values/cvalue_backward.ml
@@ -25,7 +25,7 @@ open Cvalue
let propagate_all_comparison typ =
not (Cil.isPointerType typ) ||
- Value_parameters.UndefinedPointerComparisonPropagateAll.get ()
+ Parameters.UndefinedPointerComparisonPropagateAll.get ()
let backward_int_relation typ op v1 v2 =
let v1' = V.backward_comp_int_left op v1 v2 in
@@ -35,14 +35,14 @@ let backward_int_relation typ op v1 v2 =
&& not (Cvalue_forward.are_comparable op v1 v2)
then begin
if not (Cvalue.V.equal v1 v1' || Cvalue.V.is_bottom v1') then
- Value_parameters.result
+ Self.result
~current:true ~once:true
- ~dkey:Value_parameters.dkey_pointer_comparison
+ ~dkey:Self.dkey_pointer_comparison
"not reducing %a to %a because of UPCPA" V.pretty v1 V.pretty v1';
if not (Cvalue.V.equal v2 v2' || Cvalue.V.is_bottom v2') then
- Value_parameters.result
+ Self.result
~current:true ~once:true
- ~dkey:Value_parameters.dkey_pointer_comparison
+ ~dkey:Self.dkey_pointer_comparison
"not reducing %a to %a because of UPCPA" V.pretty v2 V.pretty v2';
None
end
@@ -372,7 +372,7 @@ let downcast_enabled ~ik_src ~ik_dst =
Kernel.SignedDowncast.get () ||
(* In this case, -eva-warn-signed-converted-downcast behaves exactly
as -warn-signed-downcast *)
- (Cil.isSigned ik_src && Value_parameters.WarnSignedConvertedDowncast.get ())
+ (Cil.isSigned ik_src && Parameters.WarnSignedConvertedDowncast.get ())
else Kernel.UnsignedDowncast.get ()
(* see .mli *)
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index 1a3e65a3cc587a02bc1a96f1f968e678a6f4a434..e2996fb77f418f2e5393897749ebea8ed2d3265f 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -189,9 +189,9 @@ let assume_comparable comparison v1 v2 =
| Abstract_value.Relation ->
let truth, reason = are_comparable_reason comparison v1 v2 in
if reason <> `Ok then
- Value_parameters.result
+ Self.result
~current:true ~once:true
- ~dkey:Value_parameters.dkey_pointer_comparison
+ ~dkey:Self.dkey_pointer_comparison
"invalid pointer comparison: %a" pp_incomparable_reason reason;
truth
| Abstract_value.Subtraction ->
@@ -357,7 +357,7 @@ let forward_minus_pp ~typ ev1 ev2 =
else Ival.scale_div ~pos:true size minus_offs
with Abstract_interp.Error_Top -> Ival.top
in
- if not (Value_parameters.WarnPointerSubstraction.get ()) then
+ if not (Parameters.WarnPointerSubstraction.get ()) then
(* Generate garbled mix if the two pointers disagree on their base *)
let minus_val = V.add_untyped Int_Base.minus_one ev1 ev2 in
try
@@ -527,7 +527,7 @@ let eval_float_constant f fkind fstring =
if Fc_float.is_nan f
then V.inject_float Fval.nan
else
- let all_rounding = Value_parameters.AllRoundingModesConstants.get in
+ let all_rounding = Parameters.AllRoundingModesConstants.get in
let fl, fu = match fstring with
| Some "INFINITY" -> f, f (* Special case for the INFINITY macro. *)
| Some string when fkind = Cil_types.FLongDouble || all_rounding () ->
diff --git a/src/plugins/value/values/numerors/numerors_arithmetics.ml b/src/plugins/value/values/numerors/numerors_arithmetics.ml
index 85320659dbd099c51e367d1299da251ac2434872..50b0184d0ca43ca92f4efdbd4a69b47b5521080c 100644
--- a/src/plugins/value/values/numerors/numerors_arithmetics.ml
+++ b/src/plugins/value/values/numerors/numerors_arithmetics.ml
@@ -111,7 +111,7 @@ let non_bottom_narrow a b =
match I.narrow a b with
| `Value v -> v
| `Bottom ->
- Value_parameters.fatal
+ Self.fatal
"Numerors: a narrowing leads incorrectly to bottom.@ \
Narrow between %a@ and %a."
I.pretty a I.pretty b
diff --git a/src/plugins/value/values/numerors/numerors_float.ml b/src/plugins/value/values/numerors/numerors_float.ml
index b3816466d613ffa59d20e3cb82ac9b2440565814..079f8dfdceaa7bf2220d774f2e947295cbf0e42d 100644
--- a/src/plugins/value/values/numerors/numerors_float.ml
+++ b/src/plugins/value/values/numerors/numerors_float.ml
@@ -122,7 +122,7 @@ let neg_inf prec = of_mpfr prec @@ Mpfrf.of_float neg_infinity Mpfr.Near
*---------------------------------------------------------------------------*)
let compare (px, nx) (py, ny) =
if not (Precisions.eq px py) then
- Value_parameters.fatal
+ Self.fatal
"Numerors: impossible to compare two numbers with different precisions"
else Mpfrf.cmp nx ny
let eq a b = compare a b = 0
diff --git a/src/plugins/value/values/numerors/numerors_interval.ml b/src/plugins/value/values/numerors/numerors_interval.ml
index 98d2563bc6b30001d51b728256078f51a8a029a4..9d124f16bbcdf9f691b0860e3785f918fec836cb 100644
--- a/src/plugins/value/values/numerors/numerors_interval.ml
+++ b/src/plugins/value/values/numerors/numerors_interval.ml
@@ -51,15 +51,15 @@ let pretty fmt itv =
let prec = function NaN p -> p | I (x, _, _) -> F.prec x
let get_max_exponent = function
- | NaN _ -> Value_parameters.fatal "Numerors: can't return the exponent of a NaN"
+ | NaN _ -> Self.fatal "Numerors: can't return the exponent of a NaN"
| I (x, y, _) -> Stdlib.max (F.exponent x) (F.exponent y)
let get_exponents = function
- | NaN _ -> Value_parameters.fatal "Numerors: can't return the exponent of a NaN"
+ | NaN _ -> Self.fatal "Numerors: can't return the exponent of a NaN"
| I (x, y, _) -> F.exponent x, F.exponent y
let get_bounds = function
- | NaN _ -> Value_parameters.fatal "Numerors: can't return the bounds of a NaN"
+ | NaN _ -> Self.fatal "Numerors: can't return the bounds of a NaN"
| I (x, y, _) -> x, y
@@ -84,7 +84,7 @@ let make ?(nan = false) x y =
let bad_order = F.gt x y in
let bad_precs = not @@ Precisions.eq (F.prec x) (F.prec y) in
if there_a_nan || bad_order || bad_precs then
- Value_parameters.fatal
+ Self.fatal
"Numerors: impossible to create an interval with bounds %a and %a"
F.pretty x F.pretty y
else if F.is_pos_zero x && F.is_neg_zero y then
diff --git a/src/plugins/value/values/numerors/numerors_utils.ml b/src/plugins/value/values/numerors/numerors_utils.ml
index a58c8c8d170d7d26fbb485e8bf1a851ddcb52d4b..c0b5f95e5403102633195c8bacddce1e9c687efa 100644
--- a/src/plugins/value/values/numerors/numerors_utils.ml
+++ b/src/plugins/value/values/numerors/numerors_utils.ml
@@ -30,7 +30,7 @@ module Precisions = struct
type t = Simple | Double | Long_Double | Real
- let rp () = Value_parameters.Numerors_Real_Size.get ()
+ let rp () = Parameters.Numerors_Real_Size.get ()
let pretty fmt = function
| Simple -> Format.fprintf fmt "Simple"
@@ -125,7 +125,7 @@ module Mode = struct
type t = Abs_From_Rel | Rel_From_Abs | No_Interaction | With_Interactions
let get () =
- match Value_parameters.Numerors_Mode.get () with
+ match Parameters.Numerors_Mode.get () with
| "relative" -> Rel_From_Abs
| "absolute" -> Abs_From_Rel
| "none" -> No_Interaction