diff --git a/Makefile b/Makefile
index b99afea518b664558478423dade71ea554e0a325..abe001d1968d1b5f6f6d7fc925d3ef641eb3bc8d 100644
--- a/Makefile
+++ b/Makefile
@@ -857,9 +857,9 @@ 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 \
- utils/eva_audit utils/value_perf utils/eva_annotations \
- utils/eva_dynamic utils/value_util utils/red_statuses \
+PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
+ utils/eva_audit utils/eva_perf utils/eva_annotations \
+ utils/eva_dynamic utils/eva_utils utils/red_statuses \
utils/mark_noresults \
utils/widen_hints_ext utils/widen \
partitioning/split_return \
@@ -887,7 +887,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
domains/sign_domain \
domains/cvalue/warn domains/cvalue/locals_scoping \
domains/cvalue/cvalue_offsetmap \
- utils/value_results \
+ utils/eva_results \
utils/summary \
domains/cvalue/builtins domains/cvalue/builtins_malloc \
domains/cvalue/builtins_string domains/cvalue/builtins_misc \
@@ -932,9 +932,9 @@ 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)
+ legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli)
$(PLUGIN_DIR)/Eva.mli: $(PLUGIN_DIR)/gen-api.sh Makefile $(API_MLI)
$(PRINT_MAKING) $@
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 4a1d41dd38f7885727b646bf7f65d7a19b4aed76..0e4ca8c9bb2c2a828b8de118b3d1431e3a5fde9d 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1319,6 +1319,17 @@ src/plugins/value/Changelog_non_free: .ignore
src/plugins/value/Eva.mli: .ignore
src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/eval.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/eval.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/gen-api.sh: .ignore
+src/plugins/value/parameters.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/parameters.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/register.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/test.assert.sh: .ignore
+src/plugins/value/test.sh: .ignore
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1427,9 +1438,6 @@ src/plugins/value/engine/transfer_specification.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_specification.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_stmt.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/engine/transfer_stmt.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/eval.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/eval.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/gen-api.sh: .ignore
src/plugins/value/gui_files/gui_callstacks_filters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/gui_files/gui_callstacks_filters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/gui_files/gui_callstacks_manager.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1450,10 +1458,6 @@ src/plugins/value/legacy/eval_terms.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/legacy/eval_terms.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/legacy/function_args.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/legacy/function_args.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/register.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/register.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/results.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/results.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/auto_loop_unroll.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/auto_loop_unroll.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/partition.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1470,12 +1474,22 @@ src/plugins/value/partitioning/split_strategy.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/split_strategy.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/trace_partitioning.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/partitioning/trace_partitioning.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/test.assert.sh: .ignore
-src/plugins/value/test.sh: .ignore
src/plugins/value/utils/abstract.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/abstract.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/backward_formals.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/backward_formals.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_audit.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_dynamic.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_dynamic.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_perf.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_perf.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_results.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_results.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_utils.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_utils.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eval_typ.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eval_typ.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/red_statuses.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1484,30 +1498,18 @@ src/plugins/value/utils/library_functions.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/library_functions.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/mark_noresults.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/mark_noresults.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_annotations.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_annotations.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_audit.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_audit.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_dynamic.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/eva_dynamic.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/results.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/results.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/structure.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/summary.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/summary.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/unit_tests.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/value_perf.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/value_perf.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/value_results.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/value_results.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/value_util.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/value/utils/value_util.mli: CEA_LGPL_OR_PROPRIETARY
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/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..ee8fa22e92be08ebda0f33d3780fc160a8128f58 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. *)
@@ -450,7 +450,7 @@ module Eval_terms: sig
Cil_types.predicate -> Locations.Zone.t option
end
-module Value_results: sig
+module Eva_results: sig
type results
val get_results: unit -> results
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index e65daf45024938b8589daf977653a1725fbe491c..4b15b9a2a61e705e32caf006307f3a0d50a4bb88 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
@@ -207,7 +207,7 @@ let for_all test ~default = function
open CilE
-let emitter = Value_util.emitter
+let emitter = Eva_utils.emitter
(* Printer that shows additional information about temporaries *)
let local_printer: Printer.extensible_printer =
@@ -272,8 +272,8 @@ let loc = function
| Cil_types.Kstmt s -> Cil_datatype.Stmt.loc s
let report_alarm ki annot msg =
- Value_util.alarm_report ~source:(fst (loc ki)) "@[%s.@ @[<hov 2>%a@]@]%t"
- msg pr_annot annot Value_util.pp_callstack
+ Eva_utils.alarm_report ~source:(fst (loc ki)) "@[%s.@ @[<hov 2>%a@]@]%t"
+ msg pr_annot annot Eva_utils.pp_callstack
let string_fkind = function
| Cil_types.FFloat -> "float"
@@ -372,7 +372,7 @@ let emit_alarm kinstr alarm (status:status) =
| Alarms.Invalid_bool _ ->
register_alarm "trap representation of a _Bool lvalue"
-let height_alarm = let open Value_util in function
+let height_alarm = let open Eva_utils in function
| Alarms.Division_by_zero e
| Alarms.Index_out_of_bound (e,_)
| Alarms.Invalid_pointer e
@@ -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/api/general_requests.ml b/src/plugins/value/api/general_requests.ml
index 8d6e48f7301153d4eb7a85c70cb5e87318c433d1..54ae0cddc8d06b921dcba983059f675b46df9a09 100644
--- a/src/plugins/value/api/general_requests.ml
+++ b/src/plugins/value/api/general_requests.ml
@@ -66,7 +66,7 @@ let is_computed kf =
module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt)
let callers kf =
- let list = Value_results.callers kf in
+ let list = Eva_results.callers kf in
List.concat (List.map (fun (kf, l) -> List.map (fun s -> kf, s) l) list)
let () = Request.register ~package
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..83ac36b2b23dd36a4fb14a428834a050423c8163 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
@@ -291,7 +291,7 @@ let rec constraint_expr eval oracle env expr positive =
let typ = translate_typ (Cil.unrollType typ) in
let e = Texpr1.Binop (Texpr1.Sub, e1'', e2'', typ, round) in
let expr = Texpr1.of_expr env e in
- let binop = Value_util.conv_comp binop in
+ let binop = Eva_utils.conv_comp binop in
let binop = if positive then binop else Abstract_interp.Comp.inv binop in
translate_relation expr typ binop
| _ -> raise (Out_of_Scope "constraint_expr not handled")
@@ -495,7 +495,7 @@ module Make (Man : Input) = struct
compute state expr (Cil.typeOf expr)
let extract_lval ~oracle:_ _context state lval typ _loc =
- let expr = Value_util.lval_to_exp lval in
+ let expr = Eva_utils.lval_to_exp lval in
compute state expr typ
let maybe_bottom state =
@@ -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..57c2a2a984850adb88d2986352600e6432fca833 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)))
@@ -264,7 +264,7 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
let arguments = compute_arguments call.arguments call.rest in
try
let call_result = builtin pre arguments in
- let call_stack = Value_util.call_stack () in
+ let call_stack = Eva_utils.call_stack () in
let froms =
match call_result with
| Full result -> `Builtin result.c_from
@@ -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..437eb83a825846d5b40fdae1ec4f516e7152a787 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 ----------------------- *)
@@ -56,7 +56,7 @@ let () = Ast.add_monotonic_state Dynamic_Alloc_Bases.self
(* -------------------------- Auxiliary functions -------------------------- *)
let current_call_site () =
- match Value_util.call_stack () with
+ match Eva_utils.call_stack () with
| (_kf, Kstmt stmt) :: _ -> stmt
| _ -> Cil.dummyStmt
@@ -66,9 +66,9 @@ let current_call_site () =
these call site correspond to a different use of a malloc function,
so it is interesting to keep their bases separated. *)
let call_stack_no_wrappers () =
- let stack = Value_util.call_stack () in
+ let stack = Eva_utils.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 *)
@@ -158,16 +158,16 @@ let create_new_var stack prefix type_base weak =
| Strong -> prefix
in
let name = Cabs2cil.fresh_global (base_name prefix stack) in
- Value_util.create_new_var name type_base
+ Eva_utils.create_new_var name type_base
(* This function adds a "_w" information to a variable. It should be used
when a variable becomes weak, and supposes that the variable has been
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;
+ Eva_utils.pp_callstack;
try
let prefix, remainder =
Scanf.sscanf vi.vname "__%s@_%s" (fun s1 s2 -> (s1, s2))
@@ -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,10 +325,10 @@ 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;
+ Eva_utils.pp_callstack;
let size_char = Bit_utils.sizeofchar () in
(* Sizes are in bits *)
let min_alloc = Int.(pred (mul size_char tsize.min_bytes)) in
@@ -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 -> []
@@ -530,7 +530,7 @@ let calloc_builtin state args =
let size = Cvalue.V.mul nmemb sizev in
let size_ok = alloc_size_ok size in
if size_ok <> Alarmset.True then
- Value_util.warning_once_current
+ Eva_utils.warning_once_current
"calloc out of bounds: assert(nmemb * size <= SIZE_MAX)";
let c_values =
if size_ok = Alarmset.False (* size always overflows *)
@@ -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 *)
@@ -876,7 +876,7 @@ let check_leaked_malloced_bases state _ =
let alloced_bases = Dynamic_Alloc_Bases.get () in
Base_hptmap.iter
(fun base _ -> if check_if_base_is_leaked base state then
- Value_util.warning_once_current "memory leak detected for %a"
+ Eva_utils.warning_once_current "memory leak detected for %a"
Base.pretty base)
alloced_bases;
let c_clobbered = Base.SetLattice.bottom in
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.mli b/src/plugins/value/domains/cvalue/builtins_malloc.mli
index fecaa6ca53cc987d818429bd810e6671263d6097..9ec31b65b1c22a1d181b4a18037db57c75a7c3d4 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.mli
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.mli
@@ -36,7 +36,7 @@ val alloc_size_ok: Cvalue.V.t -> Alarmset.status
val free_automatic_bases: Value_types.Callstack.t -> Cvalue.Model.t -> Cvalue.Model.t
(** Performs the equivalent of [free] for each location that was allocated via
- [alloca()] in the current function (as per [Value_util.call_stack ()]).
+ [alloca()] in the current function (as per [Eva_utils.call_stack ()]).
This function must be called during finalization of a function call. *)
val freeable: Cvalue.V.t -> Abstract_interp.truth
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index 6309adb64fb18947419e58d53a12c82ffc069644..f3c5b263871f32e300683c9b107f675004849bf5 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,15 +84,15 @@ 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
+ V_Or_Uninitialized.pretty v Eva_utils.pp_callstack
(* Create a dependency [\from arg_n] where n is the nth argument of the
currently called function. *)
let deps_nth_arg n =
let open Function_Froms in
- let (kf,_) = List.hd (Value_util.call_stack()) in
+ let (kf,_) = List.hd (Eva_utils.call_stack()) in
try
let vi = List.nth (Kernel_function.get_formals kf) n in
Deps.add_data_dep Deps.bottom (Locations.zone_of_varinfo vi)
@@ -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,9 +240,9 @@ 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
+ Eva_utils.pp_callstack
end;
let updated_state =
Cvalue.Model.add_indeterminate_binding
@@ -600,10 +600,10 @@ 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;
+ Eva_utils.pretty_actuals actuals pretty_imprecise_memset_reason reason
+ Eva_utils.pp_callstack;
frama_c_memset_imprecise state dst v size
end
| _ -> raise (Builtins.Invalid_nb_of_args 3)
@@ -627,9 +627,9 @@ 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
+ Eva_utils.pretty_actuals actuals
end
| _ -> raise (Builtins.Invalid_nb_of_args 2)
diff --git a/src/plugins/value/domains/cvalue/builtins_misc.ml b/src/plugins/value/domains/cvalue/builtins_misc.ml
index c4112b70f8b004939b2a5bf9e0aa890e5c36e15d..3beae3f9189abdfb3a94ef851ecec4fe33db794a 100644
--- a/src/plugins/value/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_misc.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Value_util
+open Eva_utils
let frama_C_assert state actuals =
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index d73d76bde382eb383e0563235a544ff8801e88e9..2b2b2b0707be66c0ed425fefe3fbeb22f236dfaa 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,8 +282,8 @@ let state_pretty cas fmt m =
with
| Z.Overflow
| Too_large_to_enumerate ->
- Value_parameters.warning "base %s too large, \
- will not print it" name
+ Self.warning "base %s too large, \
+ will not print it" name
end
| _ -> ())
m
@@ -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..bb788c492440aac52f159b6691ac5c399d951897 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -113,18 +113,18 @@ 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
- Value_util.pp_callstack;
+ Eva_utils.pp_callstack;
if Integer.is_zero current ||
(Cil_datatype.Stmt.Set.mem stmt set)
then ()
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..f2d0655ff0227c5ba270ea489adb689a0fa3718e 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" Eva_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..67dd09d472b0a611fd210fc8eb3dbd570fcb6f52 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
@@ -62,7 +62,7 @@ type validity_hidden_base =
let stdlib_attribute = Attr ("fc_stdlib_generated", [])
let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ =
- let hidden_var = Value_util.create_new_var hidden_var_name pointed_typ in
+ let hidden_var = Eva_utils.create_new_var hidden_var_name pointed_typ in
if libc
then hidden_var.vattr <- Cil.addAttribute stdlib_attribute hidden_var.vattr;
hidden_var.vdescr <- Some name_desc;
@@ -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,8 +86,8 @@ 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 \
- size (type %a)" hidden_var_name Printer.pp_typ pointed_typ;
+ 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
| Base.Variable _ -> (* should never happen (validity_from_type cannot
@@ -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
@@ -340,7 +340,7 @@ let initialize_var_using_type varinfo state =
Cabs2cil.fresh_global ("WELL_"^name)
in
let hidden_var =
- Value_util.create_new_var hidden_var_name Cil.charType
+ Eva_utils.create_new_var hidden_var_name Cil.charType
in
hidden_var.vdescr <- Some (name_desc^"_WELL");
let validity = Base.Known (Integer.zero, Bit_utils.max_bit_address ()) in
diff --git a/src/plugins/value/domains/cvalue/cvalue_specification.ml b/src/plugins/value/domains/cvalue/cvalue_specification.ml
index fdedf776bb94083159a966c7c9085b5e978c1ccd..be23b77474b7124896818d02592919dfee9aa936 100644
--- a/src/plugins/value/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_specification.ml
@@ -66,8 +66,8 @@ 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 \
- found_indirect_deps %a stated_indirect_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;
"unknown (cannot validate "^txt^" dependencies)",
@@ -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;
@@ -151,10 +151,10 @@ let check_fct_assigns kf ab ~pre_state found_froms =
(pp_header kf) b
status_txt
pp_activity activity
- Value_util.pp_callstack;
+ Eva_utils.pp_callstack;
let emit_status ppt status =
Property_status.emit
- ~distinct:true Value_util.emitter ~hyps:[] ppt status
+ ~distinct:true Eva_utils.emitter ~hyps:[] ppt status
in
emit_status ip status;
(* Now, checks the individual froms. *)
@@ -172,7 +172,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
(pp_header kf) b
status_txt
pp_activity activity
- Value_util.pp_callstack;
+ Eva_utils.pp_callstack;
emit_status ip (conv_status status)
in
List.iter2 check_from assigns_deps assigns_zones)
diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
index 59adfa1136bf985c422ea254a7eacaf2c33c9e01..467228d64dbac95363a3359f809f992cd05d62b6 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
| _ ->
@@ -205,7 +205,7 @@ let actualize_formals state arguments =
let start_call _stmt call _recursion _valuation state =
let with_formals = actualize_formals state call.arguments in
- let stack_with_call = Value_util.call_stack () in
+ let stack_with_call = Eva_utils.call_stack () in
Db.Value.Call_Value_Callbacks.apply (with_formals, stack_with_call);
`Value with_formals
@@ -214,7 +214,7 @@ let finalize_call stmt call _recursion ~pre:_ ~post:state =
To minimize computations, only do it for function definitions. *)
let state' =
if Kernel_function.is_definition call.kf then
- let stack = (call.kf, Kstmt stmt) :: (Value_util.call_stack ()) in
+ let stack = (call.kf, Kstmt stmt) :: (Eva_utils.call_stack ()) in
Builtins_malloc.free_automatic_bases stack state
else state
in
diff --git a/src/plugins/value/domains/cvalue/warn.ml b/src/plugins/value/domains/cvalue/warn.ml
index 9f931b0f3c75ab5baf3b8161250f52f08d613e2a..ef7ecfa432145ceb7b3802ebdd382652a28f10ba 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 ->
@@ -91,7 +91,7 @@ let warn_imprecise_lval_read lv loc contents =
pretty_param_b param
Origin.pretty orig
| Location_Bytes.Map _ -> ())
- Value_util.pp_callstack
+ Eva_utils.pp_callstack
(* Auxiliary function for [do_assign] below. When computing the
result of [lv = exp], warn if the evaluation of [exp] results in
@@ -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
@@ -114,7 +114,7 @@ let warn_right_exp_imprecision lv loc_lv exp_val =
"@ @[The imprecision@ originates@ from@ %a@]"
Origin.pretty org)
origin
- Value_util.pp_callstack
+ Eva_utils.pp_callstack
| Location_Bytes.Map _ -> ()
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.ml b/src/plugins/value/domains/equality/equality.ml
index b7c63e5652b137666a50f6cb7350054c6e413e4a..f8ed19d95c233a51eb22d380640b7748169ff440 100644
--- a/src/plugins/value/domains/equality/equality.ml
+++ b/src/plugins/value/domains/equality/equality.ml
@@ -184,12 +184,12 @@ module Set = struct
let pick_representative set =
let choose elt (current, height) =
let elt = HCE.to_exp elt in
- let h = Value_util.height_expr elt in
+ let h = Eva_utils.height_expr elt in
if h < height then (elt, h) else (current, height)
in
let head = HCESet.choose set in
let current = HCE.to_exp head in
- let height = Value_util.height_expr current in
+ let height = Eva_utils.height_expr current in
fst (HCESet.fold choose (HCESet.remove head set) (current, height))
(* Binds the terms of the [equality] to [equality] in the [map].
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index ddf7bae272b9a77f854c3f3adac277e14ade6602..7c1a455765424073106a36061a5e5c54add67251 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
@@ -317,7 +317,7 @@ module Make
| Var vi, NoOffset -> Locations.zone_of_varinfo vi
| _ ->
let expr = Cil.dummy_exp (Lval lv) in
- Value_util.zone_of_expr (find_loc valuation) expr
+ Eva_utils.zone_of_expr (find_loc valuation) expr
in
Deps.add lval zone deps
@@ -398,9 +398,9 @@ module Make
let right_expr = Cil.constFold true right_expr in
try
let indirect_left_zone =
- Value_util.indirect_zone_of_lval (find_loc valuation) left_value.lval
+ Eva_utils.indirect_zone_of_lval (find_loc valuation) left_value.lval
and right_zone =
- Value_util.zone_of_expr (find_loc valuation) right_expr
+ Eva_utils.zone_of_expr (find_loc valuation) right_expr
in
(* After an assignment lv = e, the equality [lv == eq] holds iff the value
of [e] and the location of [lv] are not modified by the assignment,
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/hcexprs.ml b/src/plugins/value/domains/hcexprs.ml
index 71de08879f34c3415bd168aedcb211dd42d8d070..5b2bea75710e3e0b806e810c1578f3da4445660f 100644
--- a/src/plugins/value/domains/hcexprs.ml
+++ b/src/plugins/value/domains/hcexprs.ml
@@ -125,7 +125,7 @@ module HCE = struct
let to_exp h = match get h with
| E e -> e
- | LV lv -> Value_util.lval_to_exp lv
+ | LV lv -> Eva_utils.lval_to_exp lv
let to_lval h = match get h with
| E _ -> None
@@ -138,7 +138,7 @@ module HCE = struct
let replace kind ~late ~heir h = match get h with
| E e ->
let e = E.replace kind ~late ~heir e in
- if Value_util.height_expr e > height_limit
+ if Eva_utils.height_expr e > height_limit
then raise NonExchangeable
else of_exp e
| LV lval -> if Lval.equal lval late then of_exp heir else h
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 946b34461d059ea28d0c5cbc00a844d411cb9ef8..7b6714b25a39a7def5e05ea561da1803aea1ee77 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -162,7 +162,7 @@ module Transfer = struct
in [e] into locations. Nothing is written, the memory locations
present in [e] are read. *)
let effects_assume to_z e =
- let inputs = Value_util.zone_of_expr to_z e in
+ let inputs = Eva_utils.zone_of_expr to_z e in
{
over_outputs = Zone.bottom;
over_inputs = inputs;
@@ -173,8 +173,8 @@ module Transfer = struct
(* Effects of an assigment [lv = e]. [to_z] converts the lvalues present
in [lv] and [e] into locations. *)
let effects_assign to_z lv e =
- let inputs_e = Value_util.zone_of_expr to_z e in
- let inputs_lv = Value_util.indirect_zone_of_lval to_z lv.Eval.lval in
+ let inputs_e = Eva_utils.zone_of_expr to_z e in
+ let inputs_lv = Eva_utils.indirect_zone_of_lval to_z lv.Eval.lval in
let inputs = Zone.join inputs_e inputs_lv in
let outputs =
Precise_locs.enumerate_valid_bits Locations.Write lv.Eval.lloc
@@ -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..ac289e408eb1716fb403acef038920c94d2f2b4d 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 *)
@@ -319,7 +319,7 @@ module Rewriting = struct
|| (Ival.contains_zero ival && Ival.contains_non_zero ival)
then []
else
- let comp = Value_util.conv_comp binop in
+ let comp = Eva_utils.conv_comp binop in
let comp =
if Ival.is_zero ival then Abstract_interp.Comp.inv comp else comp
in
@@ -382,7 +382,7 @@ module Rewriting = struct
else ival, overflow_alarms typ expr ival
| BinOp ((Lt | Gt | Le | Ge | Eq as binop), e1, e2, _typ)
when Cil.isIntegralType (Cil.typeOf e1) ->
- let comp = Value_util.conv_comp binop in
+ let comp = Eva_utils.conv_comp binop in
(* Evaluate [e1 - e2] and compare the resulting interval to the interval
for which the comparison [e1 # e2] holds. *)
let range = comparison_range comp in
@@ -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..04fd2a0c8d7dafe5f561c2f94bc50e4efce8e573 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
@@ -379,7 +379,7 @@ module Memory = struct
else
let k = K.HCE.of_lval lv in
let z_lv = Precise_locs.enumerate_valid_bits Locations.Read (get_z lv) in
- let z_lv_indirect = Value_util.indirect_zone_of_lval get_z lv in
+ let z_lv_indirect = Eva_utils.indirect_zone_of_lval get_z lv in
if Locations.Zone.intersects z_lv z_lv_indirect then
(* The location of [lv] intersects with the zones needed to compute
itself, the equality would not hold. *)
@@ -395,7 +395,7 @@ module Memory = struct
state
else
let k = K.HCE.of_exp e in
- let z = Value_util.zone_of_expr get_z e in
+ let z = Eva_utils.zone_of_expr get_z e in
add_key k v z state
let find k state =
@@ -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..7a3fa0157042c13468bfbb6509ed69296b3d3b82 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
@@ -199,13 +199,13 @@ module TransferTaint = struct
let loc = Precise_locs.imprecise_location ploc in
Locations.enumerate_valid_bits Write loc
in
- let lv_indirect_zone = Value_util.indirect_zone_of_lval to_loc lval in
+ let lv_indirect_zone = Eva_utils.indirect_zone_of_lval to_loc lval in
lv_zone, lv_indirect_zone, singleton
(* Propagates data- and control-taints for an assignement [lval = exp]. *)
let assign_aux lval exp to_loc state =
let lv_zone, lv_indirect_zone, singleton = compute_zones lval to_loc in
- let exp_zone = Value_util.zone_of_expr to_loc exp in
+ let exp_zone = Eva_utils.zone_of_expr to_loc exp in
(* [lv] becomes data-tainted if a memory location on which the value of
[exp] depends on is data-tainted. *)
let data_tainted = Zone.intersects state.locs_data exp_zone in
@@ -246,7 +246,7 @@ module TransferTaint = struct
let state = filter_active_tainted_assumes stmt state in
(* Add [stmt] as assume statement in [state] as soon as [exp] is tainted. *)
let to_loc = loc_of_lval valuation in
- let exp_zone = Value_util.zone_of_expr to_loc exp in
+ let exp_zone = Eva_utils.zone_of_expr to_loc exp in
let state =
if not state.dependent_call && LatticeTaint.intersects state exp_zone
then { state with assume_stmts = Stmt.Set.add stmt state.assume_stmts; }
@@ -279,7 +279,7 @@ module TransferTaint = struct
let show_expr valuation state fmt exp =
let to_loc = loc_of_lval valuation in
- let exp_zone = Value_util.zone_of_expr to_loc exp in
+ let exp_zone = Eva_utils.zone_of_expr to_loc exp in
Format.fprintf fmt "%B" (LatticeTaint.intersects state exp_zone)
end
@@ -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..0aa29d3ba549e9afddcdfff1b73c593d24f53bb4 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,8 +386,8 @@ 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
- "The %s domain is experimental." flag.name)
+ Self.(warning ~wkey:wkey_experimental
+ "The %s domain is experimental." flag.name)
let build_domain config abstract =
let build (Flag flag, mode) acc =
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..a22d04bfebf60217422f34a2890cf1b84362ba42 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 \
- which@ a builtin@ or the specification@ will be used.@ \
- Potential unsoundness.@]" Kernel_function.pretty kf
+ 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 \
- for function '%a' for which option %s is set"
- Kernel_function.pretty kf Value_parameters.UsePrototype.option_name;
+ Self.warning "Generating potentially incorrect assigns \
+ for function '%a' for which option %s is set"
+ 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 ();
@@ -84,17 +84,17 @@ let pre_analysis () =
generate_specs ();
Widen.precompute_widen_hints ();
Builtins.prepare_builtins ();
- Value_perf.reset ();
+ Eva_perf.reset ();
(* We may be resuming Value from a previously crashed analysis. Clear
degeneration states *)
- Value_util.DegenerationPoints.clear ();
+ Eva_utils.DegenerationPoints.clear ();
Cvalue.V.clear_garbled_mix ();
- Value_util.clear_call_stack ()
+ Eva_utils.clear_call_stack ()
let post_analysis_cleanup ~aborted =
- Value_util.clear_call_stack ();
+ Eva_utils.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
@@ -105,7 +105,7 @@ let post_analysis () =
(* Garbled mix must be dumped here -- at least before the call to
mark_green_and_red -- because fresh ones are created when re-evaluating
all the alarms, and we get an unpleasant "ghost effect". *)
- Value_util.dump_garbled_mix ();
+ Eva_utils.dump_garbled_mix ();
(* Mark unreachable and RTE statuses. Only do this there, not when the
analysis was aborted (hence, not in post_cleanup), because the
propagation is incomplete. Also do not mark unreachable statutes if
@@ -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
@@ -173,24 +173,24 @@ module Make (Abstract: Abstractions.Eva) = struct
the callstack and additional information are printed. *)
let compute_using_spec_or_body call_kinstr call recursion state =
let kf = call.kf in
- Value_results.mark_kf_as_called kf;
+ Eva_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 call_stack = Value_util.call_stack () in
+ let pp = not global && Parameters.ValShowProgress.get () in
+ let call_stack = Eva_utils.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
@@ -244,26 +244,26 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
- let stack = Value_util.call_stack () in
+ let stack = Eva_utils.call_stack () in
let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
Db.Value.Call_Type_Value_Callbacks.apply (`Memexec, cvalue, stack);
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
let spec = Annotations.funspec call.kf in
- if not (Value_util.skip_specifications call.kf) &&
+ if not (Eva_utils.skip_specifications call.kf) &&
Eval_annots.has_requires spec
then begin
let ab = Logic.create init_state call.kf in
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
+ let stack_with_call = Eva_utils.call_stack () in
Db.Value.Record_Value_Callbacks_New.apply
(stack_with_call, Value_types.Reuse i);
(* call can be cached since it was cached once *)
@@ -292,12 +292,12 @@ module Make (Abstract: Abstractions.Eva) = struct
match Builtins.find_builtin_override call.kf with
| None -> compute_and_cache_call stmt call recursion state
| Some (name, builtin, cacheable, spec) ->
- Value_results.mark_kf_as_called call.kf;
+ Eva_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. *)
@@ -310,7 +310,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
- let cs = Value_util.call_stack () in
+ let cs = Eva_utils.call_stack () in
Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
@@ -337,14 +337,14 @@ module Make (Abstract: Abstractions.Eva) = struct
let () = Transfer.compute_call_ref := compute_call
let store_initial_state kf init_state =
- Abstract.Dom.Store.register_initial_state (Value_util.call_stack ()) init_state;
+ Abstract.Dom.Store.register_initial_state (Eva_utils.call_stack ()) init_state;
let cvalue_state = Abstract.Dom.get_cvalue_or_top init_state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
let compute kf init_state =
let restore_signals = register_signal_handler () in
let compute () =
- Value_util.push_call_stack kf Kglobal;
+ Eva_utils.push_call_stack kf Kglobal;
store_initial_state kf init_state;
let call =
{ kf; callstack = []; arguments = []; rest = []; return = None; }
@@ -354,8 +354,8 @@ module Make (Abstract: Abstractions.Eva) = struct
in
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;
+ Eva_utils.pop_call_stack ();
+ Self.feedback "done for function %a" Kernel_function.pretty kf;
Abstract.Dom.Store.mark_as_computed ();
post_analysis ();
Abstract.Dom.post_analysis final_state;
@@ -366,30 +366,30 @@ module Make (Abstract: Abstractions.Eva) = struct
Abstract.Dom.Store.mark_as_computed ();
post_analysis_cleanup ~aborted:true
in
- Value_util.protect compute ~cleanup
+ Eva_utils.protect compute ~cleanup
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 =
- Value_util.protect
+ Eva_utils.protect
(fun () -> Init.initial_state_with_formals ~lib_entry kf)
~cleanup:(fun () -> post_analysis_cleanup ~aborted:true)
in
match initial_state with
| `Bottom ->
Abstract.Dom.Store.mark_as_computed ();
- Value_parameters.result "Eva not started because globals \
- initialization is not computable.";
+ Self.result "Eva not started because globals \
+ initialization is not computable.";
Eval_annots.mark_invalid_initializers ()
| `Value init_state ->
compute kf init_state
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..79ac19437a81d7f8124fa2fffd4ecae58fd5da71 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
@@ -506,7 +506,7 @@ module Make
match typ with
| TFloat (fkind, _) ->
res >>= fun (value, origin) ->
- let expr = Value_util.lval_to_exp lval in
+ let expr = Eva_utils.lval_to_exp lval in
remove_special_float expr fkind value >>=: fun new_value ->
new_value, origin
| TInt (IBool, _) ->
@@ -520,7 +520,7 @@ module Make
else res
| TPtr _ ->
res >>= fun (value, origin) ->
- let expr = Value_util.lval_to_exp lval in
+ let expr = Eva_utils.lval_to_exp lval in
assume_pointer expr value >>=: fun new_value ->
new_value, origin
| _ -> res
@@ -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
@@ -627,7 +627,7 @@ module Make
| Some kind ->
let compute v1 v2 = Value.forward_binop typ_e1 op v1 v2 in
(* Detect zero expressions created by the evaluator *)
- let e1 = if Value_util.is_value_zero e1 then None else Some e1 in
+ let e1 = if Eva_utils.is_value_zero e1 then None else Some e1 in
forward_comparison ~compute typ_e1 kind (e1, v1) arg2
| None ->
assume_valid_binop typ arg1 op arg2 >>=. fun (v1, v2) ->
@@ -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)
@@ -1007,7 +1007,7 @@ module Make
in
eval_offset context ~reduce_valid_index:reduction typ offset
>>= fun (offs, typ_offs, offset_volatile) ->
- if for_writing && Value_util.is_const_write_invalid typ_offs
+ if for_writing && Eva_utils.is_const_write_invalid typ_offs
then
`Bottom,
Alarmset.singleton ~status:Alarmset.False
@@ -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
@@ -1283,7 +1283,7 @@ module Make
match expr.enode with
| Lval _lv -> assert false
| UnOp (LNot, e, _) ->
- let cond = Value_util.normalize_as_cond e false in
+ let cond = Eva_utils.normalize_as_cond e false in
(* TODO: should we compute the meet with the result of the call to
Value.backward_unop? *)
backward_eval fuel state cond (Some value)
@@ -1535,7 +1535,7 @@ module Make
result, alarms
let copy_lvalue ?(valuation=Cache.empty) ?subdivnb state lval =
- let expr = Value_util.lval_to_exp lval
+ let expr = Eva_utils.lval_to_exp lval
and context = root_context ?subdivnb state in
try
let record, report = Cache.find' valuation expr in
@@ -1588,7 +1588,7 @@ module Make
let reduce ?valuation:(valuation=Cache.empty) state expr positive =
(* Generate [e == 0] *)
- let expr = Value_util.normalize_as_cond expr (not positive) in
+ let expr = Eva_utils.normalize_as_cond expr (not positive) in
cache := valuation;
(* Currently, no subdivisions are performed during the forward evaluation
in this function, which is used to evaluate the conditions of if(…)
@@ -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..9e50efb58ac81dbc351c8491d9a61971ec053900 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,8 +273,8 @@ 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 \
- used without the Cvalue domain"
+ | 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
if (List.length formals) <> List.length actuals then
@@ -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..47959cb3306de349cd90190fd991ce756152ecd1 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 *)
@@ -129,7 +129,7 @@ module Make_Dataflow
let state = AnalysisParam.initial_state
and call_kinstr = AnalysisParam.call_kinstr
and ab = active_behaviors in
- if Value_util.skip_specifications kf then
+ if Eva_utils.skip_specifications kf then
States.singleton state
else match Logic.check_fct_preconditions call_kinstr kf ab state with
| `Bottom -> States.empty
@@ -246,9 +246,9 @@ module Make_Dataflow
let asm_contracts = Annotations.code_annot stmt in
match Logic_utils.extract_contract asm_contracts with
| [] ->
- Value_util.warning_once_current
+ Eva_utils.warning_once_current
"assuming assembly code has no effects in function %t"
- Value_util.pretty_current_cfunction_name;
+ Eva_utils.pretty_current_cfunction_name;
id
(* There should be only one statement contract, if any. *)
| (_, spec) :: _ ->
@@ -324,7 +324,7 @@ module Make_Dataflow
(* Check postconditions *)
let check_postconditions = fun state ->
post_conditions := true;
- if Value_util.skip_specifications kf then
+ if Eva_utils.skip_specifications kf then
[state]
else match
Logic.check_fct_postconditions kf active_behaviors Normal
@@ -368,7 +368,7 @@ module Make_Dataflow
(* We do not interpret annotations that come from statement contracts
and everything previously emitted by Value (currently, alarms) *)
let filter e ca =
- not (Logic_utils.is_contract ca || Emitter.equal e Value_util.emitter)
+ not (Logic_utils.is_contract ca || Emitter.equal e Eva_utils.emitter)
in
List.map fst (Annotations.code_annot_emitter ~filter stmt)
in
@@ -448,7 +448,7 @@ module Make_Dataflow
let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
Db.Value.Compute_Statement_Callbacks.apply
- (stmt, Value_util.call_stack (), cvalue_states)
+ (stmt, Eva_utils.call_stack (), cvalue_states)
let update_vertex ?(widening : bool = false) (v : vertex)
(sources : ('branch * flow) list) : bool =
@@ -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
@@ -586,7 +586,7 @@ module Make_Dataflow
let f stmt (v,_) =
let l = get_succ_tanks v in
if not (List.for_all Partitioning.is_empty_tank l) then
- Value_util.DegenerationPoints.replace stmt false
+ Eva_utils.DegenerationPoints.replace stmt false
in
StmtTable.iter f automaton.stmt_table;
match !current_ki with
@@ -594,7 +594,7 @@ module Make_Dataflow
| Kstmt s ->
let englobing_kf = Kernel_function.find_englobing_kf s in
if Kernel_function.equal englobing_kf kf then (
- Value_util.DegenerationPoints.replace s true)
+ Eva_utils.DegenerationPoints.replace s true)
(* If the postconditions have not been evaluated, mark them as true. *)
let mark_postconds_as_true () =
@@ -698,7 +698,7 @@ module Make_Dataflow
in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
and merged_post_cvalues = lazy (lift_to_cvalues merged_post_states) in
- let callstack = Value_util.call_stack () in
+ let callstack = Eva_utils.call_stack () in
if Mark_noresults.should_memorize_function fundec then begin
let register_pre = Domain.Store.register_state_before_stmt callstack
and register_post = Domain.Store.register_state_after_stmt callstack 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,13 +774,13 @@ 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
if Cil.hasAttribute "noreturn" f.svar.vattr && results <> [] then
- Value_util.warning_once_current
+ Eva_utils.warning_once_current
"function %a may terminate but has the noreturn attribute"
Kernel_function.pretty kf;
results, !Dataflow.cacheable
@@ -789,7 +789,7 @@ module Computer
Dataflow.mark_degeneration ();
Dataflow.merge_results ()
in
- Value_util.protect compute ~cleanup
+ Eva_utils.protect compute ~cleanup
end
diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml
index 71c6807a8fec3367044cdfc1717b4e4722b2629f..079654be5e5583f74db158557aca313474f09796 100644
--- a/src/plugins/value/engine/recursion.ml
+++ b/src/plugins/value/engine/recursion.ml
@@ -31,7 +31,7 @@ let mark_unknown_requires kinstr kf funspec =
| Kglobal -> assert false
| Kstmt stmt -> stmt
in
- let emitter = Value_util.emitter in
+ let emitter = Eva_utils.emitter in
let status = Property_status.Dont_know in
let emit_behavior behavior =
let emit_predicate predicate =
@@ -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,17 +56,17 @@ 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;
+ Eva_utils.pp_callstack;
Cil.CurrentLoc.set (Kernel_function.get_location kf);
ignore (!Annotations.populate_spec_ref kf funspec);
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..6b96d072f172037eb5c3c6a49706efd25bb564fe 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;
@@ -708,7 +708,7 @@ module Make
(* Builds the information for an lvalue. *)
let get_info context valuation lval =
- let lv_expr = Value_util.lval_to_exp lval in
+ let lv_expr = Eva_utils.lval_to_exp lval in
(* Reevaluates the lvalue in the initial state, as its value could have
been reduced in the evaluation of the complete expression, and we cannot
omit the alarms for the removed values. *)
@@ -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..9c474bf23cb30f00d6b816f5dc941b04725e6ed0 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -69,16 +69,16 @@ let emit_status ppt status =
if status = Property_status.False_if_reachable then begin
Red_statuses.add_red_property (Property.get_kinstr ppt) ppt;
end;
- Property_status.emit ~distinct:true Value_util.emitter ~hyps:[] ppt status
+ Property_status.emit ~distinct:true Eva_utils.emitter ~hyps:[] 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
+ Eva_utils.alarm_report ?current ?once ?source fmt
let behavior_inactive fmt =
Format.fprintf fmt " (Behavior may be inactive, no reduction performed.)"
@@ -123,7 +123,7 @@ let emit_message_and_status kind kf behavior ~active ~empty property named_pred
pp_predicate named_pred
Alarmset.Status.pretty status
(if active then (fun _ -> ()) else behavior_inactive)
- Value_util.pp_callstack;
+ Eva_utils.pp_callstack;
emit_status property (conv_status status);
| Postcondition postk ->
(* Do not emit a status for leaf functions or builtins. Otherwise, we would
@@ -236,9 +236,9 @@ 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
+ (pp_header kf) behavior Eva_utils.pp_callstack
let process_inactive_behaviors call_ki kf behaviors =
List.iter (process_inactive_behavior kf call_ki) behaviors
@@ -258,9 +258,9 @@ 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;
+ (pp_header kf) b Eva_utils.pp_callstack;
) inactive_bhvs
(* -------------------------------- Functor --------------------------------- *)
@@ -421,14 +421,14 @@ 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 \
incomplete@ (or incorrect).@]%t"
pp_header behavior
(if active then (fun _ -> ()) else pp_behavior_inactive)
- Value_util.pp_callstack
+ Eva_utils.pp_callstack
(* [per_behavior] indicates if we are processing each behavior separately.
If this is the case, then [Unknown] and [True] behaviors are treated
@@ -453,7 +453,7 @@ module Make
- [build_env] is used to build the environment evaluation, in particular
the pre- and post-states. *)
let eval_and_reduce kf behavior active kind ips states build_prop build_env =
- let limit = Value_util.get_slevel kf in
+ let limit = Eva_utils.get_slevel kf in
let emit = emit_message_and_status kind kf behavior ~active in
let aux_pred states pred =
let pr = Logic_const.pred_of_id_pred pred in
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index 6c953deb3d14074c32383002bb96566a30f65cdf..aab9b10deef6b7310de87c99046023a73e1b481c 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -40,7 +40,7 @@ let find_default_behavior spec =
List.find (fun b' -> b'.b_name = Cil.default_behavior_name) spec.spec_behavior
let warn_empty_assigns () =
- Value_util.warning_once_current
+ Eva_utils.warning_once_current
"Cannot handle empty assigns clause. Assuming assigns \\nothing: \
be aware this is probably incorrect."
@@ -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)
@@ -109,9 +109,9 @@ let warn_on_missing_result_assigns kinstr kf spec =
let return_used = match kinstr with
| Kglobal -> true
| Kstmt {skind = Instr (Call (lv, _, _, _))} ->
- lv <> None || Value_util.postconditions_mention_result spec
+ lv <> None || Eva_utils.postconditions_mention_result spec
| Kstmt {skind = Instr (Local_init(_,ConsInit(_,_,Constructor),_)) } ->
- Value_util.postconditions_mention_result spec
+ Eva_utils.postconditions_mention_result spec
| Kstmt {skind=Instr(Local_init(_,ConsInit(_,_,Plain_func),_))} -> true
| _ -> assert false
in
@@ -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
@@ -164,7 +164,7 @@ let precise_loc_of_assign env kind term =
in
if kind <> From then reduce_to_valid_location kind term loc else Some loc
with Eval_terms.LogicEvalError e ->
- Value_util.warning_once_current
+ Eva_utils.warning_once_current
"@[<hov 0>@[<hov 2>cannot interpret %a@]%a;@ effects will be ignored@]"
pp_assign_clause (kind, term) pp_eval_error e;
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..47358794f67e3e190617d78e9ede7d24087e9dd2 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
@@ -88,10 +88,10 @@ let is_determinate kf =
(warn_indeterminate kf || !Db.Value.use_spec_instead_of_definition kf)
&& not (Ast_info.is_frama_c_builtin name)
-let subdivide_stmt = Value_util.get_subdivision
+let subdivide_stmt = Eva_utils.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
@@ -243,7 +243,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Bottom ->
Kernel.warning ~current:true ~once:true
"@[<v>@[all target addresses were invalid. This path is \
- assumed to be dead.@]%t@]" Value_util.pp_callstack;
+ assumed to be dead.@]%t@]" Eva_utils.pp_callstack;
`Bottom
| `Value (valuation, lloc, ltyp) ->
(* Tries to interpret the assignment as a copy for the returned value
@@ -312,9 +312,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Returns the result of a call, and a boolean that indicates whether a
builtin has been used to interpret the call. *)
let process_call stmt call recursion valuation state =
- Value_util.push_call_stack call.kf (Kstmt stmt);
+ Eva_utils.push_call_stack call.kf (Kstmt stmt);
let cleanup () =
- Value_util.pop_call_stack ();
+ Eva_utils.pop_call_stack ();
(* Changed by compute_call_ref, called from process_call *)
Cil.CurrentLoc.set (Cil_datatype.Stmt.loc stmt);
in
@@ -324,7 +324,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Process the call according to the domain decision. *)
match Domain.start_call stmt call recursion domain_valuation state with
| `Value state ->
- Domain.Store.register_initial_state (Value_util.call_stack ()) state;
+ Domain.Store.register_initial_state (Eva_utils.call_stack ()) state;
!compute_call_ref stmt call recursion state
| `Bottom ->
{ states = []; cacheable = Cacheable; builtin=false }
@@ -332,7 +332,7 @@ module Make (Abstract: Abstractions.Eva) = struct
cleanup ();
res
in
- Value_util.protect process
+ Eva_utils.protect process
~cleanup:(fun () -> InOutCallback.clear (); cleanup ())
(* ------------------- Retro propagation on formals ----------------------- *)
@@ -363,7 +363,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Top -> Precise_locs.loc_top
| `Value record -> get record.loc
in
- let expr_zone = Value_util.zone_of_expr find_loc expr in
+ let expr_zone = Eva_utils.zone_of_expr find_loc expr in
let written_zone = inout.Inout_type.over_outputs_if_termination in
not (Locations.Zone.intersects expr_zone written_zone)
@@ -440,7 +440,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| None, Some vi_ret -> `Value (Domain.leave_scope kf_callee [vi_ret] state)
| Some _, None -> assert false
| Some lval, Some vi_ret ->
- let exp_ret_caller = Value_util.lval_to_exp (Var vi_ret, NoOffset) in
+ let exp_ret_caller = Eva_utils.lval_to_exp (Var vi_ret, NoOffset) in
assign_ret state (Kstmt stmt) lval exp_ret_caller
>>-: fun state -> Domain.leave_scope kf_callee [vi_ret] state
@@ -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)
@@ -534,7 +534,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Create an Eval.call *)
let create_call kf args =
let return = Library_functions.get_retres_vi kf in
- let callstack = Value_util.call_stack () in
+ let callstack = Eva_utils.call_stack () in
let arguments, rest =
let formals = Kernel_function.get_formals kf in
let rec format_arguments acc args formals = match args, formals with
@@ -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,15 +599,15 @@ 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
+ name print_state state Eva_utils.pp_callstack
(* Idem as for [print_state]. *)
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,9 +627,9 @@ 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
+ name pp arguments Eva_utils.pp_callstack
(* For non scalar expressions, prints the offsetmap of the cvalue domain. *)
let show_offsm =
@@ -672,9 +672,9 @@ 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
+ name (pretty_arguments ~subdivnb state) arguments Eva_utils.pp_callstack
(* Frama_C_dump_each_file functions. *)
let dump_state_file_exc ~subdivnb name arguments state =
@@ -691,8 +691,8 @@ 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"
- file Value_util.pp_callstack;
+ Self.feedback ~current:true "Dumping state in file '%s'%t"
+ file Eva_utils.pp_callstack;
Format.fprintf fmt "DUMPING STATE at file %a line %d@."
Datatype.Filepath.pretty l.Filepath.pos_path
l.Filepath.pos_lnum;
@@ -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)
@@ -728,10 +728,10 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Legacy callbacks for the cvalue domain, usually called by
{Cvalue_transfer.start_call}. *)
let apply_cvalue_callback kf ki_call state =
- let stack_with_call = (kf, ki_call) :: Value_util.call_stack () in
+ let stack_with_call = (kf, ki_call) :: Eva_utils.call_stack () in
let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
- Db.Value.merge_initial_state (Value_util.call_stack ()) cvalue_state;
+ Db.Value.merge_initial_state (Eva_utils.call_stack ()) cvalue_state;
Db.Value.Call_Type_Value_Callbacks.apply
(`Builtin None, cvalue_state, stack_with_call)
@@ -749,7 +749,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let cacheable = ref Cacheable in
let eval =
functions >>-: fun functions ->
- let current_kf = Value_util.current_kf () in
+ let current_kf = Eva_utils.current_kf () in
let process_one_function kf valuation =
(* The special Frama_C_ functions to print states are handled here. *)
if apply_special_directives ~subdivnb kf args state
@@ -763,7 +763,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let states =
eval >>-: fun (call, recursion, valuation) ->
(* Register the call. *)
- Value_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
+ Eva_results.add_kf_caller call.kf ~caller:(current_kf, stmt);
(* Do the call. *)
let c, states =
do_one_call valuation stmt lval_option call recursion state
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..2b2cb3425ba21500297751bc07361f91c0f7b8ee 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 =
@@ -162,7 +162,7 @@ let active_highlighter buffer localizable ~start ~stop =
let degenerate =
try
Some (
- if Value_util.DegenerationPoints.find stmt
+ if Eva_utils.DegenerationPoints.find stmt
then (make_tag buffer ~name:"degeneration" [`BACKGROUND "orange"])
else (make_tag buffer ~name:"unpropagated" [`BACKGROUND "yellow"])
)
@@ -234,7 +234,7 @@ let cleaned_outputs kf s =
let pretty_stmt_info (main_ui:main_ui) kf stmt =
(* Is it an accessible statement ? *)
if Results.is_reachable stmt then begin
- if Value_results.is_non_terminating_instr stmt then
+ if Eva_results.is_non_terminating_instr stmt then
match stmt.skind with
| Instr (Call (_, _, _, _)
| Local_init (_, ConsInit _, _)) ->
@@ -520,7 +520,7 @@ module Select (Eval: Eval) = struct
| Mem _, NoOffset when Cil.isFunctionType ty -> begin
(* Function pointers *)
(* get the list of functions in the values *)
- let e = Value_util.lval_to_exp lv in
+ let e = Eva_utils.lval_to_exp lv in
let state =
match ki with
| Kglobal -> Eval.Analysis.get_global_state ()
diff --git a/src/plugins/value/legacy/eval_annots.ml b/src/plugins/value/legacy/eval_annots.ml
index 68aed0aadab7bc2b5171980bd0962f7b4f3e8c94..910bb4dfce767536d0ef9979ceed4c5dfab04443 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -46,10 +46,10 @@ 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:[]
+ Property_status.emit ~distinct:false Eva_utils.emitter ~hyps:[]
in
let reach_p = Property.ip_reachable_ppt ppt in
emit ppt Property_status.True;
@@ -73,7 +73,7 @@ let mark_unreachable () =
let mark_status kf =
(* Do not mark preconditions as dead if they are not analyzed in
non-dead code. Otherwise, the consolidation does strange things. *)
- if not (Value_util.skip_specifications kf) ||
+ if not (Eva_utils.skip_specifications kf) ||
Builtins.is_builtin_overridden kf
then begin
(* Setup all precondition statuses for [kf]: maybe it has
@@ -187,10 +187,10 @@ let mark_green_and_red () =
| `True -> Property_status.True, "valid"
| `False -> Property_status.False_if_reachable, "invalid"
in
- Property_status.emit ~distinct Value_util.emitter ~hyps:[] ip status;
+ Property_status.emit ~distinct Eva_utils.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
@@ -230,7 +230,7 @@ let mark_invalid_initializers () =
let status = Property_status.False_and_reachable in
let distinct = false (* see comment in mark_green_and_red above *) in
Red_statuses.add_red_property Kglobal ip;
- Property_status.emit ~distinct Value_util.emitter ~hyps:[] ip status;
+ Property_status.emit ~distinct Eva_utils.emitter ~hyps:[] ip status;
end
| _ -> ()
in
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..ec1f608362e8d54a05ca368e77c39472b9644eb1 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
@@ -985,7 +985,7 @@ let forward_binop_by_type typ =
let forward_binop typ v1 op v2 =
match op with
| Eq | Ne | Le | Lt | Ge | Gt ->
- let comp = Value_util.conv_comp op in
+ let comp = Eva_utils.conv_comp op in
if Cil.isPointerType typ || Cvalue_forward.are_comparable comp v1 v2
then forward_binop_by_type typ v1 op v2
else Cvalue.V.zero_or_one
@@ -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;
@@ -1983,7 +1983,7 @@ and reduce_by_left_relation ~alarm_mode env positive tl rel tr =
let exact_location = eval_term_as_exact_locs ~alarm_mode env tl in
let rtl = eval_term ~alarm_mode env tr in
let cond_v = rtl.eover in
- let comp = Value_util.conv_relation rel in
+ let comp = Eva_utils.conv_relation rel in
match exact_location with
| Logic_var logic_var ->
let cvalue = LogicVarEnv.find logic_var env.logic_vars in
@@ -2395,7 +2395,7 @@ and eval_predicate env pred =
in
let typ_pointed = Logic_typing.ctype_of_pointed tsets.term_type in
(* Check if we are trying to write in a const l-value *)
- if kind = Write && Value_util.is_const_write_invalid typ_pointed
+ if kind = Write && Eva_utils.is_const_write_invalid typ_pointed
then False
else
let eover, eunder, indeterminate, empty =
@@ -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..8f851352d8140efd44ce9282449c60bec8fb3af9 100644
--- a/src/plugins/value/partitioning/per_stmt_slevel.ml
+++ b/src/plugins/value/partitioning/per_stmt_slevel.ml
@@ -70,7 +70,7 @@ let kf_contains_slevel_directive kf =
(Kernel_function.get_definition kf).sallstmts
let compute kf =
- let default_slevel = Value_util.get_slevel kf in
+ let default_slevel = Eva_utils.get_slevel kf in
if not (kf_contains_slevel_directive kf) then
Global default_slevel (* No slevel directive *), NoMerge
else
@@ -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..8bf1ae4ac30d4fcb06cce1f7a649a7663e6b84a0 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
@@ -257,7 +257,7 @@ module Eval = struct
bot_value (eval >>-: snd)
let eval_lval ?with_alarms deps state lval =
- let expr = Value_util.lval_to_exp lval in
+ let expr = Eva_utils.lval_to_exp lval in
let res, valuation = eval_expr_with_valuation ?with_alarms deps state expr in
let typ = match valuation with
| None -> Cil.typeOfLval lval
@@ -413,7 +413,7 @@ module Export (Eval : Eval) = struct
let lval_to_zone_with_deps_state state ~for_writing ~deps lv =
let deps, r = lval_to_precise_loc_with_deps_state state ~deps lv in
let r = (* No write effect if [lv] is const *)
- if for_writing && (Value_util.is_const_write_invalid (Cil.typeOfLval lv))
+ if for_writing && (Eva_utils.is_const_write_invalid (Cil.typeOfLval lv))
then Precise_locs.loc_bottom
else r
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/backward_formals.ml b/src/plugins/value/utils/backward_formals.ml
index e01d275dd7f2c3555e384886330b9afcd7476e0f..48e98b856b1a2afbf5084b88512e4915c7cf5495 100644
--- a/src/plugins/value/utils/backward_formals.ml
+++ b/src/plugins/value/utils/backward_formals.ml
@@ -79,7 +79,7 @@ module WrittenFormals =
(struct
let size = 17
let dependencies = [Ast.self]
- let name = "Value_util.WrittenFormals"
+ let name = "Eva_utils.WrittenFormals"
end)
let written_formals = WrittenFormals.memo written_formals
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/value_perf.ml b/src/plugins/value/utils/eva_perf.ml
similarity index 98%
rename from src/plugins/value/utils/value_perf.ml
rename to src/plugins/value/utils/eva_perf.ml
index 5d1d845e294d1fcac34816b8f2821c8cf04ba20f..66f45a43f9c48b809c33365a6ed2bbc0e1b22f4f 100644
--- a/src/plugins/value/utils/value_perf.ml
+++ b/src/plugins/value/utils/eva_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_perf.mli b/src/plugins/value/utils/eva_perf.mli
similarity index 100%
rename from src/plugins/value/utils/value_perf.mli
rename to src/plugins/value/utils/eva_perf.mli
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/eva_results.ml
similarity index 97%
rename from src/plugins/value/utils/value_results.ml
rename to src/plugins/value/utils/eva_results.ml
index d8dfd0c0fd3dda6aa95f9695d5df5a2829b5de77..bab62ba7d48b4ffb1f96b39223e7a617d0d90117 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/eva_results.ml
@@ -28,7 +28,7 @@ module Is_Called =
Kernel_function.Make_Table
(Datatype.Bool)
(struct
- let name = "Value.Value_results.is_called"
+ let name = "Value.Eva_results.is_called"
let dependencies = [ Db.Value.self ]
let size = 17
end)
@@ -49,7 +49,7 @@ module Callers =
Kernel_function.Make_Table
(Kernel_function.Map.Make(Stmt.Set))
(struct
- let name = "Value.Value_results.Callers"
+ let name = "Value.Eva_results.Callers"
let dependencies = [ Db.Value.self ]
let size = 17
end)
@@ -116,7 +116,7 @@ type stmt_by_callstack = Cvalue.Model.t Value_types.Callstack.Hashtbl.t
module AlarmsStmt =
Datatype.Pair_with_collections (Alarms) (Stmt)
- (struct let module_name = "Value.Value_results.AlarmStmt" end)
+ (struct let module_name = "Value.Eva_results.AlarmStmt" end)
type results = {
main: Kernel_function.t option (** None means multiple functions *);
@@ -134,7 +134,7 @@ type results = {
}
let get_results () =
- let vue = Emitter.get Value_util.emitter in
+ let vue = Emitter.get Eva_utils.emitter in
let main = Some (fst (Globals.entry_point ())) in
let module CS = Value_types.Callstack in
let copy_states iter =
@@ -245,12 +245,12 @@ let set_results results =
(* Alarms *)
let aux_alarms (alarm, stmt) st =
let ki = Cil_types.Kstmt stmt in
- ignore (Alarms.register Value_util.emitter ki ~status:st alarm)
+ ignore (Alarms.register Eva_utils.emitter ki ~status:st alarm)
in
AlarmsStmt.Hashtbl.iter aux_alarms results.alarms;
(* Statuses *)
let aux_statuses ip st =
- Property_status.emit Value_util.emitter ~hyps:[] ip st
+ Property_status.emit Eva_utils.emitter ~hyps:[] ip st
in
Property.Hashtbl.iter aux_statuses results.statuses;
Db.Value.mark_as_computed ();
diff --git a/src/plugins/value/utils/value_results.mli b/src/plugins/value/utils/eva_results.mli
similarity index 100%
rename from src/plugins/value/utils/value_results.mli
rename to src/plugins/value/utils/eva_results.mli
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/eva_utils.ml
similarity index 90%
rename from src/plugins/value/utils/value_util.ml
rename to src/plugins/value/utils/eva_utils.ml
index cd0d402e1f9da9f64142f1ba106955cbc0b73b3c..5f0438cc7808d0da495efcff1220fb40ff3c7769 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/eva_utils.ml
@@ -31,13 +31,13 @@ let clear_call_stack () =
call_stack := []
let pop_call_stack () =
- Value_perf.stop_doing !call_stack;
+ Eva_perf.stop_doing !call_stack;
call_stack := List.tl !call_stack
;;
let push_call_stack kf ki =
call_stack := (kf,ki) :: !call_stack;
- Value_perf.start_doing !call_stack
+ Eva_perf.start_doing !call_stack
;;
@@ -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,18 +91,18 @@ 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 =
Cil_state_builder.Stmt_hashtbl
(Datatype.Bool)
(struct
- let name = "Value_util.Degeneration"
+ let name = "Eva_utils.Degeneration"
let size = 17
let dependencies = [ Db.Value.self ]
end)
@@ -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 =
@@ -238,13 +238,13 @@ let rec normalize_as_cond expr positive =
module PairExpBool =
Datatype.Pair_with_collections(Cil_datatype.Exp)(Datatype.Bool)
- (struct let module_name = "Value.Value_util.PairExpBool" end)
+ (struct let module_name = "Value.Eva_utils.PairExpBool" end)
module MemoNormalizeAsCond =
State_builder.Hashtbl
(PairExpBool.Hashtbl)
(Cil_datatype.Exp)
(struct
- let name = "Value_util.MemoNormalizeAsCond"
+ let name = "Eva_utils.MemoNormalizeAsCond"
let size = 64
let dependencies = [ Ast.self ]
end)
@@ -255,7 +255,7 @@ module MemoLvalToExp =
Cil_state_builder.Lval_hashtbl
(Cil_datatype.Exp)
(struct
- let name = "Value_util.MemoLvalToExp"
+ let name = "Eva_utils.MemoLvalToExp"
let size = 64
let dependencies = [ Ast.self ]
end)
@@ -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/eva_utils.mli
similarity index 97%
rename from src/plugins/value/utils/value_util.mli
rename to src/plugins/value/utils/eva_utils.mli
index c99393d8885d66b5e1e11023582e3b7b797f05c7..b784b933c600a19a959c61838a07c48e38b503fb 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/eva_utils.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/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index 9d729c7e8eb674c3a03612de4ee59f89a84e3f77..c9b81edc45245610137f78afe256624bd9b5e691 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,9 +62,9 @@ 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;
+ Eva_utils.pp_callstack;
Cvalue.V.top_int
| TVoid _ -> Cvalue.V.top (* this value will never be used *)
| TFun _ | TNamed _ | TArray _ -> assert false
@@ -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..903319a436be509cb32fcace07f57c78b6e9b324 100644
--- a/src/plugins/value/utils/red_statuses.ml
+++ b/src/plugins/value/utils/red_statuses.ml
@@ -76,7 +76,7 @@ let add_red_ap kinstr ap =
try AlarmOrProp.Map.find ap current_map
with Not_found -> Callstacks.empty
in
- let new_callstacks = Callstacks.add (Value_util.call_stack ()) callstacks in
+ let new_callstacks = Callstacks.add (Eva_utils.call_stack ()) callstacks in
let new_map = AlarmOrProp.Map.add ap new_callstacks current_map in
RedStatusesTable.replace kinstr new_map
@@ -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/results.ml b/src/plugins/value/utils/results.ml
index 87a2ee9758f3ede02bd347959d77a58f4da61270..bcea5fd3c1f539eba40c2de0117ac6427e6e3d22 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -371,7 +371,7 @@ struct
let as_zone ~access res =
let response_loc, lv = extract_loc res in
- let is_const_lv = Value_util.is_const_write_invalid (Cil.typeOfLval lv) in
+ let is_const_lv = Eva_utils.is_const_write_invalid (Cil.typeOfLval lv) in
(* No write effect if [lv] is const *)
if access=Locations.Write && is_const_lv
then Result.ok Locations.Zone.bottom
diff --git a/src/plugins/value/utils/summary.ml b/src/plugins/value/utils/summary.ml
index 1429c0262b314bff082b941cf0e2fe9d495a1245..2ed7573fe071ad06ebb97d39ae6cdf641cc0ecf8 100644
--- a/src/plugins/value/utils/summary.ml
+++ b/src/plugins/value/utils/summary.ml
@@ -148,7 +148,7 @@ end
(* --- Function stats computation --- *)
let get_status ip =
- let eva_emitter = Value_util.emitter in
+ let eva_emitter = Eva_utils.emitter in
let aux_status emitter status acc =
let emitter = Emitter.Usable_emitter.get emitter.Property_status.emitter in
if Emitter.equal eva_emitter emitter
@@ -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/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..97c67f3aade2df6333bfb2fc874b37149f29731b 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
@@ -276,7 +276,7 @@ let backward_binop ~typ_res ~res_value ~typ_e1 v1 binop v2 =
(* comparison operators *)
| (Eq | Ne | Le | Lt | Ge | Gt), _ -> begin
- let binop = Value_util.conv_comp binop in
+ let binop = Eva_utils.conv_comp binop in
match V.is_included V.singleton_zero res_value,
V.is_included V.singleton_one res_value with
| true, true ->
@@ -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..cc48ef0c78aed6b42658f906f4a76df24a9dcff5 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
@@ -402,7 +402,7 @@ let forward_binop_int ~typ ev1 op ev2 =
~contains_zero: (V.contains_zero ev1 || V.contains_zero ev2)
~contains_non_zero:(V.contains_non_zero ev1 && V.contains_non_zero ev2)
| Eq | Ne | Ge | Le | Gt | Lt ->
- let op = Value_util.conv_comp op in
+ let op = Eva_utils.conv_comp op in
let signed = Bit_utils.is_signed_int_enum_pointer (Cil.unrollType typ) in
V.inject_comp_result (V.forward_comp_int ~signed op ev1 ev2)
@@ -420,7 +420,7 @@ let forward_binop_float fkind ev1 op ev2 =
| Mult -> binary_float_floats "*." Fval.mul
| Div -> binary_float_floats "/." Fval.div
| Eq | Ne | Lt | Gt | Le | Ge ->
- let op = Value_util.conv_comp op in
+ let op = Eva_utils.conv_comp op in
V.inject_comp_result (Fval.forward_comp op f1 f2)
| _ -> assert false
@@ -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 () ->
@@ -539,7 +539,7 @@ let eval_float_constant f fkind fstring =
if Fc_float.is_infinite f_lower && Fc_float.is_infinite f_upper
then
begin
- Value_util.warning_once_current
+ Eva_utils.warning_once_current
"cannot parse floating-point constant, returning imprecise result";
neg_infinity, infinity
end
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
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 08334941537bb65fd0931def46400ca033e12a12..b951eefd39f71757399e2e856172bd5e0d992a16 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -315,7 +315,7 @@ let backward_comp_right op ~left ~right =
let backward_binop ~input_type:_ ~resulting_type:_ op ~left ~right ~result =
match op with
| Ne | Eq | Le | Lt | Ge | Gt ->
- let op = Value_util.conv_comp op in
+ let op = Eva_utils.conv_comp op in
if equal zero result then
(* The comparison is false, as it always evaluate to false. Reduce by the
fact that the inverse comparison is true. *)