From 33732f51aebcb298787c2d7fa84309a437a0f3d1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 14 Feb 2022 17:20:58 +0100
Subject: [PATCH] [Eva] Results: [as_cvalue] converts error cases into bottom
or top cvalue.
New function [as_cvalue_result] returns error cases without conversion.
---
src/plugins/constant_propagation/api.ml | 3 +--
src/plugins/dive/build.ml | 3 +--
src/plugins/value/Eva.mli | 6 +++++-
src/plugins/value/utils/results.ml | 10 ++++++++--
src/plugins/value/utils/results.mli | 6 +++++-
5 files changed, 20 insertions(+), 8 deletions(-)
diff --git a/src/plugins/constant_propagation/api.ml b/src/plugins/constant_propagation/api.ml
index 2b3bf770836..be5eb41d5d1 100644
--- a/src/plugins/constant_propagation/api.ml
+++ b/src/plugins/constant_propagation/api.ml
@@ -135,8 +135,7 @@ class propagate project fnames ~cast_intro = object(self)
| None -> raise Cannot_change
| Some s -> s
in
- let evaled = Eva.Results.(
- before stmt |> eval_exp expr |> as_cvalue |> default Cvalue.V.top) in
+ let evaled = Eva.Results.(before stmt |> eval_exp expr |> as_cvalue) in
let b, m = Cvalue.V.find_lonely_binding evaled in
let can_replace vi =
(* can replace the current expr by [vi] iff (1) it is a source var, or
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index af26fe2d1f8..b694d6d85ec 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -82,8 +82,7 @@ struct
Result.value ~default:[]
let to_cvalue kinstr lval =
- before_kinstr kinstr |> eval_lval lval |> as_cvalue |>
- Result.value ~default:Cvalue.V.bottom
+ before_kinstr kinstr |> eval_lval lval |> as_cvalue
let to_location kinstr lval =
before_kinstr kinstr |> eval_address lval |> as_location |>
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 6e4c7a769a4..58006b2c451 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -228,8 +228,12 @@ module Results: sig
(** Converts the value into a floating point abstraction. *)
val as_fval : value evaluation -> Fval.t result
+ (** Converts the value into a Cvalue abstraction. Converts error cases
+ into bottom and top values accordingly. *)
+ val as_cvalue : value evaluation -> Cvalue.V.t
+
(** Converts the value into a Cvalue abstraction. *)
- val as_cvalue : value evaluation -> Cvalue.V.t result
+ val as_cvalue_result : value evaluation -> Cvalue.V.t result
(** Converts into a C location abstraction. *)
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index c61dbb8f510..87a2ee9758f 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -553,13 +553,19 @@ let callee stmt =
(* Value conversion *)
-let as_cvalue (Value evaluation) =
+let as_cvalue_result (Value evaluation) =
let module E = (val evaluation : Evaluation) in
E.as_cvalue E.v
+let as_cvalue evaluation =
+ match as_cvalue_result evaluation with
+ | Ok v -> v
+ | Error Bottom -> Cvalue.V.bottom
+ | Error (Top | DisabledDomain) -> Cvalue.V.top
+
let as_ival evaluation =
try
- Result.map Cvalue.V.project_ival (as_cvalue evaluation)
+ Result.map Cvalue.V.project_ival (as_cvalue_result evaluation)
with Cvalue.V.Not_based_on_null ->
Result.error Top
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index 53251203bb1..e24441ccb68 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -216,8 +216,12 @@ val as_ival : value evaluation -> Ival.t result
(** Converts the value into a floating point abstraction. *)
val as_fval : value evaluation -> Fval.t result
+(** Converts the value into a Cvalue abstraction. Converts error cases
+ into bottom and top values accordingly. *)
+val as_cvalue : value evaluation -> Cvalue.V.t
+
(** Converts the value into a Cvalue abstraction. *)
-val as_cvalue : value evaluation -> Cvalue.V.t result
+val as_cvalue_result : value evaluation -> Cvalue.V.t result
(** Converts into a C location abstraction. *)
--
GitLab