diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index c17ab76acb1bcbe64590960ea72e3796dfeb37dc..af26fe2d1f894f8b9da96a68438fa6abcacdf519 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -90,8 +90,7 @@ struct
Result.value ~default:Locations.loc_bottom
let to_zone kinstr lval =
- before_kinstr kinstr |> eval_address lval |> as_zone |>
- Result.value ~default:Locations.Zone.bottom
+ before_kinstr kinstr |> eval_address lval |> as_zone
let to_callstacks stmt =
before stmt |> callstacks
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index f7bec37f39e3be3928d06129200804beaf5c6fd2..5976c3b6f0fafc7bcc6e3e495609392e96e47bf7 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -52,7 +52,7 @@ class virtual do_it_ = object(self)
let bits_loc = Eva.Results.(
before_kinstr self#current_kinstr |> eval_address lv |>
as_zone ~access) in
- Result.iter self#join bits_loc
+ self#join bits_loc
method! vinst i =
if Db.Value.is_reachable (Db.Value.noassert_get_state self#current_kinstr)
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index cbf6feb70846cf1dd57df3a5b3accf76e580e99d..5e6922a3562dd445f1ea22a8ace1b3468dfeb956 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -107,20 +107,18 @@ class occurrence = object (self)
method! vlval lv =
let ki = self#current_kinstr in
begin
- match Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) with
- | Result.Error _ -> (* ignore *) ()
- | Ok z ->
- try
- Locations.Zone.fold_topset_ok
- (fun b _ () ->
- match b with
- | Base.Var (vi, _) | Base.Allocated (vi, _, _) ->
- Occurrences.add vi self#current_kf ki lv
- | _ -> ()
- ) z ()
- with Abstract_interp.Error_Top ->
- error ~current:true "Found completely imprecise value (%a). Ignoring@."
- Printer.pp_lval lv
+ let z = Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) in
+ try
+ Locations.Zone.fold_topset_ok
+ (fun b _ () ->
+ match b with
+ | Base.Var (vi, _) | Base.Allocated (vi, _, _) ->
+ Occurrences.add vi self#current_kf ki lv
+ | _ -> ()
+ ) z ()
+ with Abstract_interp.Error_Top ->
+ error ~current:true "Found completely imprecise value (%a). Ignoring@."
+ Printer.pp_lval lv
end;
DoChildren
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index b3782a1a193ace3b6e604edb1e3db82eba10d28e..6bc2734636b51ba4793e4ac3910deca6cffc49db 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -81,9 +81,7 @@ module InitSid = struct
end
let get_writes stmt lval =
- Eva.Results.(
- before stmt |> eval_address lval |> as_zone ~access:Write |>
- default Locations.Zone.bottom)
+ Eva.Results.(before stmt |> eval_address lval |> as_zone ~access:Write)
(** Add to [stmt] to [lmap] for all the locations modified by the statement.
* Something to do only for calls and assignments.
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index 0aede3dd05eff5646b3cdc2e6f74a6edb3c975ac..af1e23d78388266822ed34f6e8bbad847c6ef558 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -168,8 +168,7 @@ let compute kf stmt lval =
in
Eva.Analysis.compute ();
let zone = Eva.Results.(before stmt |> eval_address lval |> as_zone) in
- Option.bind (Result.to_option zone) (compute_aux kf stmt) |>
- Option.map extract
+ compute_aux kf stmt zone |> Option.map extract
(* Variation of the function above. For each PDG node that has been found,
we find whether it directly modifies [zone] through an affectation
@@ -220,8 +219,7 @@ let compute_with_def_type_zone kf stmt zone =
let compute_with_def_type kf stmt lval =
Eva.Analysis.compute ();
let zone =
- Eva.Results.(before stmt |> eval_address lval |> as_zone) |>
- Result.value ~default:Locations.Zone.bottom
+ Eva.Results.(before stmt |> eval_address lval |> as_zone)
in
compute_with_def_type_zone kf stmt zone
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index cdfb8be1be922c17ed06c8e95349136ae6d1fcfe..8340d52e18cffd804ca5e09c873a6bfa1d634920 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -58,7 +58,6 @@ let get_select_kf (fvar, _select) = Globals.Functions.get fvar
let get_lval_zone ?(access=Locations.Read) stmt lval =
let open Eva.Results in
before stmt |> eval_address lval |> as_zone ~access
- |> default Locations.Zone.bottom
(** Utilities for [kinstr]. *)
module Kinstr: sig
diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml
index f1a94a67bd23fcdd8d289fa96ff300961348781d..2e44a1b8e8f0d4c9503225954eefa4578b65d3b9 100644
--- a/src/plugins/studia/studia_request.ml
+++ b/src/plugins/studia/studia_request.ml
@@ -82,9 +82,7 @@ let compute kind zone =
List.fold_left add empty stmts
let lval_location kinstr lval =
- Eva.Results.(
- before_kinstr kinstr |> eval_address lval |> as_zone |>
- default Locations.Zone.bottom)
+ Eva.Results.(before_kinstr kinstr |> eval_address lval |> as_zone)
let () = Request.register ~package
~kind:`GET ~name:"getReadsLval"
diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml
index d323327d03be5af511b1e409e4e2acaeedaa294e..dbcbcfc04cea20a2596da29b264f3ea0e4b852ee 100644
--- a/src/plugins/studia/writes.ml
+++ b/src/plugins/studia/writes.ml
@@ -66,7 +66,7 @@ class find_write zlval = object (self)
let direct_write = match lvopt with
| None -> false
| Some lv ->
- Eva.Results.(before stmt |> eval_address lv |> as_zone) |>
+ Eva.Results.(before stmt |> eval_address lv |> as_zone_result) |>
Result.fold ~ok:(Zone.intersects zlval) ~error:(fun _ -> false)
in
let effects =
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 75e6e742e821b29918a35be15802c0e4857e8589..d6281ebcd41e119df0079346574c85087e8b7782 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -203,8 +203,12 @@ module Results: sig
(** Converts into a C location abstraction. *)
val as_location : address evaluation -> Locations.location result
- (** Converts into a Zone. *)
- val as_zone : ?access:Locations.access -> address evaluation ->
+ (** Converts into a Zone. Error cases are converted into bottom or top zones
+ accordingly. *)
+ val as_zone: ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t
+ (** Converts into a Zone result. *)
+ val as_zone_result : ?access:Locations.access -> address evaluation ->
Locations.Zone.t result
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index ea5c066bf7ab04c067fbaadd7fabe565067339d3..3bcf3b4da4d3e803ce2e586f50208ae17ba56cce 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -695,10 +695,16 @@ let as_location (Address lvaluation) =
let module E = (val lvaluation : Lvaluation) in
E.as_location E.v
-let as_zone ?(access=Locations.Read) (Address lvaluation) =
+let as_zone_result ?(access=Locations.Read) (Address lvaluation) =
let module E = (val lvaluation : Lvaluation) in
E.as_zone ~access E.v
+let as_zone ?access address =
+ match as_zone_result ?access address with
+ | Ok zone -> zone
+ | Error Bottom -> Locations.Zone.bottom
+ | Error (Top | DisabledDomain) -> Locations.Zone.top
+
(* Evaluation properties *)
let is_initialized (Value evaluation) =
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index 74e9b67936b48106ccc21aaf2504228a3040acf7..b3580445ded176b6ea2e06ca031255cfac27ae77 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -191,8 +191,12 @@ val as_cvalue : value evaluation -> Cvalue.V.t result
(** Converts into a C location abstraction. *)
val as_location : address evaluation -> Locations.location result
-(** Converts into a Zone. *)
-val as_zone : ?access:Locations.access -> address evaluation ->
+(** Converts into a Zone. Error cases are converted into bottom or top zones
+ accordingly. *)
+val as_zone: ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t
+(** Converts into a Zone result. *)
+val as_zone_result : ?access:Locations.access -> address evaluation ->
Locations.Zone.t result