From 8a633be26ae3dd6f50b76cae546dc13bb03a2484 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Mar 2021 11:43:52 +0100
Subject: [PATCH] [Eva] Eval_terms: removes some global open.
---
src/plugins/value/legacy/eval_terms.ml | 48 +++++++++++++-------------
1 file changed, 24 insertions(+), 24 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 8bd86bc341e..ff080649717 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -21,15 +21,12 @@
(**************************************************************************)
open Cil_types
-open Cil_datatype
open Locations
-open Abstract_interp
open Cvalue
-open Bit_utils
(* Truth values for a predicate analyzed by the value analysis *)
-type predicate_status = Comp.result = True | False | Unknown
+type predicate_status = Abstract_interp.Comp.result = True | False | Unknown
let string_of_predicate_status = function
| Unknown -> "unknown"
@@ -172,6 +169,7 @@ let contains_invalid_loc access loc =
to force its re-evaluation.
*)
+module Logic_label = Cil_datatype.Logic_label
type labels_states = Cvalue.Model.t Logic_label.Map.t
let join_label_states m1 m2 =
@@ -319,9 +317,9 @@ let bind_logic_vars env lvs =
| Lreal -> bind_logic_var top_float
| Ctype ctyp when Cil.isIntegralType ctyp ->
let base = Base.of_c_logic_var lv in
- let size = Int.of_int (Cil.bitsSizeOf ctyp) in
+ let size = Integer.of_int (Cil.bitsSizeOf ctyp) in
let v = Cvalue.V_Or_Uninitialized.initialized V.top_int in
- let state = Model.add_base_value base ~size v ~size_v:Int.one state in
+ let state = Model.add_base_value base ~size v ~size_v:Integer.one state in
state, logic_vars
| _ -> unsupported_lvar lv
in
@@ -581,17 +579,17 @@ let pass_logic_cast exn typ trm =
match Logic_utils.unroll_type typ, Logic_utils.unroll_type trm.term_type with
| Linteger, Ctype (TInt _ | TEnum _) -> () (* Always inclusion *)
| Ctype (TInt _ | TEnum _ as typ), Ctype (TInt _ | TEnum _ as typeoftrm) ->
- let sztyp = sizeof typ in
- let szexpr = sizeof typeoftrm in
+ let sztyp = Bit_utils.sizeof typ in
+ let szexpr = Bit_utils.sizeof typeoftrm in
let styp, sexpr =
match sztyp, szexpr with
| Int_Base.Value styp, Int_Base.Value sexpr -> styp, sexpr
| _ -> raise exn
in
- let sityp = is_signed_int_enum_pointer typ in
- let sisexpr = is_signed_int_enum_pointer typeoftrm in
- if (Int.ge styp sexpr && sityp = sisexpr) (* larger, same signedness *)
- || (Int.gt styp sexpr && sityp) (* strictly larger and signed *)
+ let sityp = Bit_utils.is_signed_int_enum_pointer typ in
+ let sisexpr = Bit_utils.is_signed_int_enum_pointer typeoftrm in
+ if (Integer.ge styp sexpr && sityp = sisexpr) (* larger, same signedness *)
+ || (Integer.gt styp sexpr && sityp) (* strictly larger and signed *)
then ()
else raise exn
@@ -626,7 +624,7 @@ let constraint_trange idx size_arr =
in
let up = match up with (* constrained r.h.s *)
| Some _ -> up
- | None -> Some (Logic_const.tint ~loc (Int.pred size))
+ | None -> Some (Logic_const.tint ~loc (Integer.pred size))
in
Logic_const.trange ~loc (low, up)
end
@@ -721,8 +719,8 @@ let inline logic_info =
and the \Positive and \Negative constructors (handled in eval_term). They can
only be compared through equality and disequality; no other operation exists
on this type, so our interpretation remains correct. *)
-let positive_cvalue = Cvalue.V.inject_int Int.one
-let negative_cvalue = Cvalue.V.inject_int Int.minus_one
+let positive_cvalue = Cvalue.V.inject_int Integer.one
+let negative_cvalue = Cvalue.V.inject_int Integer.minus_one
let is_true = function
| `True | `TrueReduced _ -> true
@@ -799,7 +797,7 @@ let eval_logic_charlen wrapper env v ldeps =
let eover =
let v, alarms = apply_logic_builtin wrapper env [v] in
if alarms && not (Cvalue.V.is_bottom v)
- then Cvalue.V.inject_ival (Ival.inject_range (Some Int.minus_one) None)
+ then Cvalue.V.inject_ival (Ival.inject_range (Some Integer.minus_one) None)
else v
in
let eunder = under_from_over eover in
@@ -1253,11 +1251,11 @@ let rec eval_term ~alarm_mode env t =
frontiers are always 0 or 8*k-1 (because validity is in bits and
starts on zero), so we add 1 everywhere, then divide by eight. *)
let convert start_bits end_bits =
- let congr_succ i = Int.(equal zero (e_rem (succ i) eight)) in
- let congr_or_zero i = Int.(equal zero i || congr_succ i) in
+ let congr_succ i = Integer.(equal zero (e_rem (succ i) eight)) in
+ let congr_or_zero i = Integer.(equal zero i || congr_succ i) in
assert (congr_or_zero start_bits || congr_or_zero end_bits);
- let start_bytes = Int.(e_div (Int.succ start_bits) eight) in
- let end_bytes = Int.(e_div (Int.succ end_bits) eight) in
+ let start_bytes = Integer.(e_div (Integer.succ start_bits) eight) in
+ let end_bytes = Integer.(e_div (Integer.succ end_bits) eight) in
Ival.inject_range (Some start_bytes) (Some end_bytes)
in
match Base.validity b with
@@ -1445,7 +1443,8 @@ and eval_known_logic_function ~alarm_mode env li labels args =
| ("\\min" | "\\max"), Some typ, _, t1 :: t2 :: tail_args ->
begin
- let comp = if lvi.lv_name = "\\min" then Comp.Le else Comp.Ge in
+ let min = lvi.lv_name = "\\min" in
+ let comp = Abstract_interp.Comp.(if min then Le else Ge) in
let backward =
match typ with
| Linteger -> Cvalue.V.backward_comp_int_left comp
@@ -1919,7 +1918,7 @@ and reduce_by_valid env positive access (tset: term) =
in
let li = if op = PlusPI then li else Ival.neg_int li in
let typ_p = Cil.typeOf_pointed rtlv.etype in
- let sbits = Int.of_int (Cil.bitsSizeOf typ_p) in
+ let sbits = Integer.of_int (Cil.bitsSizeOf typ_p) in
(* Compute the offsets expected by [aux], which are [i *
8 * sizeof( *tlv)] *)
let li = Ival.scale sbits li in
@@ -2550,6 +2549,7 @@ and eval_predicate env pred =
(* Logic predicates. Update the list known_predicates above if you
add something here. *)
and eval_known_papp env li _labels args =
+ let open Abstract_interp in
let unary_float unary_fun arg =
try
let eval_result = eval_term ~alarm_mode env arg in
@@ -2692,12 +2692,12 @@ let predicate_deps env pred =
empty_logic_deps args
else
match Inline.inline_predicate ~inline ~current:env.e_cur p with
- | None -> unsupported (Format.asprintf "%a" Predicate.pretty p)
+ | None -> unsupported (Format.asprintf "%a" Printer.pp_predicate p)
| Some p' -> do_eval env p'
end
| Pfresh _ | Pallocable _ | Pfreeable _
- -> unsupported (Format.asprintf "%a" Predicate.pretty p)
+ -> unsupported (Format.asprintf "%a" Printer.pp_predicate p)
in
try Some (do_eval env pred)
with LogicEvalError _ -> None
--
GitLab