diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index 708a6bb9a50d744faa2854e790b2ba2c913b36d2..6dadf905432720fc1089f1ccbeb39f5434681146 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 ca2a5e8fcb0556ee08a9ab93ec75349fcec2e309..a28f266db67266116c1963b3fabba62e8fe82413 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 *)