diff --git a/Makefile b/Makefile
index 90d05c020d39381a0b657499a5447d421b06850d..2f0fc8b59ca8f41fdfefd74ed19a1fc6dde540bc 100644
--- a/Makefile
+++ b/Makefile
@@ -859,7 +859,7 @@ endif
# - try to keep the legacy Value before Eva
PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode self parameters \
utils/eva_audit utils/value_perf utils/eva_annotations \
- utils/eva_dynamic utils/value_util utils/red_statuses \
+ utils/eva_dynamic utils/eva_utils utils/red_statuses \
utils/mark_noresults \
utils/widen_hints_ext utils/widen \
partitioning/split_return \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 730ba7179805c2a0447060ea7e9fe6bf50016dfc..deed26f01a3305d4dea9fd43324bbac8f307b104 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1500,8 +1500,8 @@ 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/eva_utils.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/eva_utils.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
diff --git a/src/plugins/value/alarmset.ml b/src/plugins/value/alarmset.ml
index e6ce2b905c4024e602c04268a19a73cf742a036b..4b15b9a2a61e705e32caf006307f3a0d50a4bb88 100644
--- a/src/plugins/value/alarmset.ml
+++ b/src/plugins/value/alarmset.ml
@@ -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
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index c044bc41e10f51e8c93ce2b91960d8b6ff0f05a8..83ac36b2b23dd36a4fb14a428834a050423c8163 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -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 =
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 6a06c6e95e23e1b5b9f88610ad064028827a0a5d..57c2a2a984850adb88d2986352600e6432fca833 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -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
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index c6197530c239f399dec5a5ddb7f85e2e1e6714b5..437eb83a825846d5b40fdae1ec4f516e7152a787 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -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,7 +66,7 @@ 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 = Parameters.AllocFunctions.get() in
let rec bottom_filter = function
@@ -158,7 +158,7 @@ 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
@@ -167,7 +167,7 @@ let create_new_var stack prefix type_base weak =
let mutate_name_to_weak vi =
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))
@@ -328,7 +328,7 @@ let alloc_fresh weak deallocation prefix sizev _state =
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
@@ -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 *)
@@ -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 d40cc1db42d8b7f6a3dc2d9bf6765a5715448c1f..f3c5b263871f32e300683c9b107f675004849bf5 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -86,13 +86,13 @@ let memcpy_check_indeterminate_offsetmap offsm =
with Indeterminate v ->
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)
@@ -242,7 +242,7 @@ let frama_c_memcpy state actuals =
| V_Or_Uninitialized.C_init_noesc _ -> ()
| _ -> 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
@@ -602,8 +602,8 @@ let frama_c_memset state actuals =
with ImpreciseMemset reason ->
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)
@@ -629,7 +629,7 @@ let frama_c_interval_split _state actuals =
| Ival.Not_Singleton_Int ->
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_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index 3507dcea92bceb60c5b068076971d8d40c3e6386..bb788c492440aac52f159b6691ac5c399d951897 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -117,7 +117,7 @@ let watch_hook (stmt, _callstack, states) =
"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 ()
diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml
index ee6a2bbebbba3f420d8878ae0c161d322e4bb875..efb1cdabfa0f1b193dc4083249313317c52e3668 100644
--- a/src/plugins/value/domains/cvalue/cvalue_init.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_init.ml
@@ -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;
@@ -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 ac5b5396cab61c311f75e2c48fd0c1e4f76fc121..61e2004f1327fe7bb36c0bf1d1be1dc6d77c774b 100644
--- a/src/plugins/value/domains/cvalue/cvalue_specification.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_specification.ml
@@ -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 874865e8abae16d543aece59090cc1dd8e36cae9..467228d64dbac95363a3359f809f992cd05d62b6 100644
--- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml
@@ -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 0ac785c335db88a8a994f2b836e415bc7d96160b..ef7ecfa432145ceb7b3802ebdd382652a28f10ba 100644
--- a/src/plugins/value/domains/cvalue/warn.ml
+++ b/src/plugins/value/domains/cvalue/warn.ml
@@ -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
@@ -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/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 a237f1f912278e6a5b8898af183dcccba337333c..7c1a455765424073106a36061a5e5c54add67251 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -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/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 87f4ac0fa15bfa9fdfd9471c56cc20058cc517bd..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
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 79d4426df919c2d24adbd2710828548fbdc41a48..ac289e408eb1716fb403acef038920c94d2f2b4d 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -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
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 65cdb97b9a767a3eba9907b1b74cb2a904cd9864..04fd2a0c8d7dafe5f561c2f94bc50e4efce8e573 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -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 =
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 8ba90e4ceb9317f1afc05a983318d3963951d4a9..7a3fa0157042c13468bfbb6509ed69296b3d3b82 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -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
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 30b31b9a20ac839f81baf14f926e3bfdd5e2658d..27e5fc92c8b19fbd5a85bd5cab6ee7dc8f841a05 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -87,12 +87,12 @@ let pre_analysis () =
Value_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 Parameters.JoinResults.get () then
Db.Value.Table_By_Callstack.iter
@@ -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
@@ -176,7 +176,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Value_results.mark_kf_as_called kf;
let global = match call_kinstr with Kglobal -> true | _ -> false in
let pp = not global && Parameters.ValShowProgress.get () in
- let call_stack = Value_util.call_stack () in
+ let call_stack = Eva_utils.call_stack () in
if pp then
Self.feedback
"@[computing for function %a.@\nCalled from %a.@]"
@@ -244,13 +244,13 @@ 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
@@ -263,7 +263,7 @@ module Make (Abstract: Abstractions.Eva) = struct
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 *)
@@ -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,7 +354,7 @@ 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 ();
+ Eva_utils.pop_call_stack ();
Self.feedback "done for function %a" Kernel_function.pretty kf;
Abstract.Dom.Store.mark_as_computed ();
post_analysis ();
@@ -366,7 +366,7 @@ 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 ();
@@ -374,7 +374,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(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
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 58ba02483a7986b94991e8de5ef7a0126d40f992..79ac19437a81d7f8124fa2fffd4ecae58fd5da71 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -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
@@ -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) ->
@@ -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
@@ -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(…)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 7e5856b22451e42bfcc4257f3140d08070313cc9..47959cb3306de349cd90190fd991ce756152ecd1 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -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 =
@@ -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
@@ -780,7 +780,7 @@ module Computer
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 69c13c26cfc1ea57cc91846c5fc8d4c646c28884..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 =
@@ -58,7 +58,7 @@ let get_spec kinstr kf =
Kernel_function.pretty kf
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
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index ac077da8bab2e217c5b40909fcf413af0b2c74fc..6b96d072f172037eb5c3c6a49706efd25bb564fe 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -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. *)
diff --git a/src/plugins/value/engine/transfer_logic.ml b/src/plugins/value/engine/transfer_logic.ml
index dc07aad5c0143bbe49a14bb01b919541679ca632..9c474bf23cb30f00d6b816f5dc941b04725e6ed0 100644
--- a/src/plugins/value/engine/transfer_logic.ml
+++ b/src/plugins/value/engine/transfer_logic.ml
@@ -69,7 +69,7 @@ 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 =
@@ -78,7 +78,7 @@ let msg_status status ?current ?once ?source fmt =
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
@@ -238,7 +238,7 @@ let process_inactive_behavior kf call_ki behavior =
if !emitted then
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
@@ -260,7 +260,7 @@ let process_inactive_postconds kf inactive_bhvs =
if !emitted then
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 --------------------------------- *)
@@ -428,7 +428,7 @@ module Make
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 92ece96f4d1c52df7816f354f6b4491e79fb3ed8..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."
@@ -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
@@ -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
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 005d88b1eb4070cfe89e734ab5448a07b160a9c4..47f623da748b6b38341bc244fd1bb5575cca1c8b 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -88,7 +88,7 @@ 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 -> Parameters.LinearLevel.get ()
@@ -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
@@ -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
@@ -601,7 +601,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let dump_state name state =
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 =
@@ -629,7 +629,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let pp = Pretty_utils.pp_list ~pre:"@[<v>" ~sep:"@ " ~suf:"@]" pretty in
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 =
@@ -674,7 +674,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let show_each ~subdivnb name arguments state =
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 =
@@ -692,7 +692,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let fmt = Format.formatter_of_out_channel ch in
let l = fst (Cil.CurrentLoc.get ()) in
Self.feedback ~current:true "Dumping state in file '%s'%t"
- file Value_util.pp_callstack;
+ 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;
@@ -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
diff --git a/src/plugins/value/gui_files/register_gui.ml b/src/plugins/value/gui_files/register_gui.ml
index 750c7e92888f3106cb404ad8f37b3763024de25b..ed3146c0e9977738cc7fbfd65abe855436b6075a 100644
--- a/src/plugins/value/gui_files/register_gui.ml
+++ b/src/plugins/value/gui_files/register_gui.ml
@@ -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"])
)
@@ -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 0baae6b9a5fb373299b2f8ff66bb9e193ab85356..910bb4dfce767536d0ef9979ceed4c5dfab04443 100644
--- a/src/plugins/value/legacy/eval_annots.ml
+++ b/src/plugins/value/legacy/eval_annots.ml
@@ -49,7 +49,7 @@ let mark_unreachable () =
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,7 +187,7 @@ 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
Self.result ~once:true ~source "%s%a got final status %s."
@@ -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_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 34a39cd38c3a3ec19db78105c7802633ca1eaa45..ec1f608362e8d54a05ca368e77c39472b9644eb1 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -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
@@ -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 =
diff --git a/src/plugins/value/partitioning/per_stmt_slevel.ml b/src/plugins/value/partitioning/per_stmt_slevel.ml
index 4631d81e56bfdd5b4ff34f0659dbfdbfae1c9dfb..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
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index 4d242ad2cdfa4295ea1f081b8f73cf72253850e9..8bf1ae4ac30d4fcb06cce1f7a649a7663e6b84a0 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -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/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/value_util.ml b/src/plugins/value/utils/eva_utils.ml
similarity index 98%
rename from src/plugins/value/utils/value_util.ml
rename to src/plugins/value/utils/eva_utils.ml
index a3c7470b3ef60d7ce16a48f7d4bc25e80365d021..f92d43efb582f3e9e13dfb0fa476328f605a5490 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/eva_utils.ml
@@ -102,7 +102,7 @@ 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)
@@ -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)
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/eva_utils.mli
similarity index 100%
rename from src/plugins/value/utils/value_util.mli
rename to src/plugins/value/utils/eva_utils.mli
diff --git a/src/plugins/value/utils/library_functions.ml b/src/plugins/value/utils/library_functions.ml
index 4b6ddb5553fc66e35ccd94b2e7a49192999af032..c9b81edc45245610137f78afe256624bd9b5e691 100644
--- a/src/plugins/value/utils/library_functions.ml
+++ b/src/plugins/value/utils/library_functions.ml
@@ -64,7 +64,7 @@ let returned_value kf =
| TBuiltin_va_list _ ->
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
diff --git a/src/plugins/value/utils/red_statuses.ml b/src/plugins/value/utils/red_statuses.ml
index a326f184a2c517c19941b2d5c09896dd4d190e0c..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
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 a56f47b4ec1983cac86380c565e0433e163a85af..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
diff --git a/src/plugins/value/utils/value_results.ml b/src/plugins/value/utils/value_results.ml
index d8dfd0c0fd3dda6aa95f9695d5df5a2829b5de77..3547690f300c53f0086c5e14da41afb723af6cad 100644
--- a/src/plugins/value/utils/value_results.ml
+++ b/src/plugins/value/utils/value_results.ml
@@ -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/values/cvalue_backward.ml b/src/plugins/value/values/cvalue_backward.ml
index 0993a32bba3725c629cb9cd164c208142ef2f8d8..97c67f3aade2df6333bfb2fc874b37149f29731b 100644
--- a/src/plugins/value/values/cvalue_backward.ml
+++ b/src/plugins/value/values/cvalue_backward.ml
@@ -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 ->
diff --git a/src/plugins/value/values/cvalue_forward.ml b/src/plugins/value/values/cvalue_forward.ml
index e2996fb77f418f2e5393897749ebea8ed2d3265f..cc48ef0c78aed6b42658f906f4a76df24a9dcff5 100644
--- a/src/plugins/value/values/cvalue_forward.ml
+++ b/src/plugins/value/values/cvalue_forward.ml
@@ -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
@@ -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/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. *)