Merge branch 'feature/eva/is-singleton' into 'master'

[Eva] Results: exports function [is_singleton].

See merge request frama-c/frama-c!3663

src/plugins/value/Eva.mli

@@ -252,6 +252,11 @@ module Results: sig
 
   (** Evaluation properties *)
 
+
+  (** Does the evaluated abstraction represents only one possible C value or
+      memory location? *)
+  val is_singleton : 'a evaluation -> bool
+
   (** Returns whether the evaluated value is initialized or not. If the value have
       been evaluated from a Cil expression, it is always initialized. *)
   val is_initialized : value evaluation -> bool

src/plugins/value/utils/results.ml

@@ -599,6 +599,17 @@ let as_zone address =
 
 (* Evaluation properties *)
 
+let is_singleton: type a. a evaluation -> bool = function
+  | Value _ as evaluation ->
+    let cvalue = as_cvalue evaluation in
+    Cvalue.V.cardinal_zero_or_one cvalue && not (Cvalue.V.is_bottom cvalue)
+  | Address _ as lvaluation ->
+    let loc = as_location lvaluation in
+    let is_singleton loc =
+      Locations.cardinal_zero_or_one loc && not (Locations.is_bottom_loc loc)
+    in
+    Result.fold ~ok:is_singleton ~error:(fun _ -> false) loc
+
 let is_initialized (Value evaluation) =
   let module E = (val evaluation : Evaluation) in
   E.is_initialized E.v

src/plugins/value/utils/results.mli

@@ -239,6 +239,11 @@ val as_zone_result : address evaluation -> Locations.Zone.t result
 
 (** Evaluation properties *)
 
+
+(** Does the evaluated abstraction represents only one possible C value or
+    memory location? *)
+val is_singleton : 'a evaluation -> bool
+
 (** Returns whether the evaluated value is initialized or not. If the value have
     been evaluated from a Cil expression, it is always initialized. *)
 val is_initialized : value evaluation -> bool