Merge branch 'feature/eva/api-cvalue-or-uninit' into 'master'

[Eva] Results API: implements new function [as_cvalue_or_uninitialized].

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

src/plugins/value/utils/results.ml

@@ -315,6 +315,29 @@ struct
 
   (* Conversion *)
 
+  let as_cvalue_or_uninitialized res =
+    match A.Val.get Main_values.CVal.key with
+    | None -> `Top
+    | Some get ->
+      let make_expr (x, _alarms) =
+        x >>>-: fun (_valuation, v) ->
+        Cvalue.V_Or_Uninitialized.make ~initialized:true ~escaping:false (get v)
+      in
+      let make_lval (x, _alarms) =
+        x >>>-: fun (_valuation, v) ->
+        let Eval.{ v; initialized; escaping } = v in
+        let v =
+          match v with
+          | `Bottom -> Cvalue.V.bottom
+          | `Value v -> get v
+        in
+        Cvalue.V_Or_Uninitialized.make ~initialized ~escaping v
+      in
+      let join = Cvalue.V_Or_Uninitialized.join in
+      match res with
+      | LValue r -> Response.map_join' make_lval join r
+      | Value r -> Response.map_join' make_expr join r
+
   let extract_value :
     type c. (value, c) evaluation -> (A.Val.t or_bottom, c) Response.t =
     function
@@ -539,6 +562,13 @@ let callee stmt =
 
 (* Value conversion *)
 
+let as_cvalue_or_uninitialized (Value evaluation) =
+  let module E = (val evaluation : Evaluation) in
+  match E.as_cvalue_or_uninitialized E.v with
+  | `Value v -> v
+  | `Bottom -> Cvalue.V_Or_Uninitialized.bottom
+  | `Top -> Cvalue.V_Or_Uninitialized.top
+
 let as_cvalue_result (Value evaluation) =
   let module E = (val evaluation : Evaluation) in
   E.as_cvalue E.v

src/plugins/value/utils/results.mli

@@ -225,6 +225,10 @@ val as_cvalue : value evaluation -> Cvalue.V.t
 (** Converts the value into a Cvalue abstraction. *)
 val as_cvalue_result : value evaluation -> Cvalue.V.t result
 
+(** Converts the value into a Cvalue abstraction with 'undefined' and 'escaping
+    addresses' flags. *)
+val as_cvalue_or_uninitialized : value evaluation -> Cvalue.V_Or_Uninitialized.t
+
 
 (** Converts into a C location abstraction. *)
 val as_location : address evaluation -> Locations.location result