From f8b0626f5079abbf5448a2cc01fbd6bca6362dcb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 18 Jul 2022 21:47:26 +0200
Subject: [PATCH] [Eva] Results: exports [as_precise_loc] and
 [as_precise_loc_result].

[as_precise_loc] converts error cases in bottom or top precise_locs accordingly.
---
 src/plugins/eva/Eva.mli           | 8 ++++++++
 src/plugins/eva/utils/results.mli | 8 ++++++++
 2 files changed, 16 insertions(+)

diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 708a6bb9a50..6dadf905432 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -363,6 +363,14 @@ module Results: sig
   (** Converts into a Zone result. *)
   val as_zone_result : address evaluation -> Locations.Zone.t result
 
+  (** Converts into a C location abstraction. Error cases are converted into
+      bottom or top locations accordingly. *)
+  val as_precise_loc : address evaluation -> Precise_locs.precise_location
+
+  (** Converts into a C location abstraction. *)
+  val as_precise_loc_result :
+    address evaluation -> Precise_locs.precise_location result
+
 
   (** Evaluation properties *)
 
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index ca2a5e8fcb0..a28f266db67 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -268,6 +268,14 @@ val as_zone: address evaluation -> Locations.Zone.t
 (** Converts into a Zone result. *)
 val as_zone_result : address evaluation -> Locations.Zone.t result
 
+(** Converts into a C location abstraction. Error cases are converted into
+    bottom or top locations accordingly. *)
+val as_precise_loc : address evaluation -> Precise_locs.precise_location
+
+(** Converts into a C location abstraction. *)
+val as_precise_loc_result :
+  address evaluation -> Precise_locs.precise_location result
+
 
 (** Evaluation properties *)
 
-- 
GitLab