Merge branch 'feature/eva/ivette-values-initialization' into 'master'

[Eva] Fixes values requests on uninitialized or escaping lvalues

Closes #1239

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

src/plugins/eva/api/general_requests.ml

@@ -216,6 +216,13 @@ let property_evaluation_point = function
 let marker_evaluation_point = function
   | Printer_tag.PGlobal _ -> Initial
   | PStmt (kf, stmt) | PStmtStart (kf, stmt) -> Stmt (kf, stmt)
+  | PVDecl (kf, kinstr, v) when not (v.vformal || v.vglob) ->
+    begin
+      (* Only evaluate declaration of local variable if it is initialized. *)
+      match kf, kinstr with
+      | Some kf, Kstmt ({skind = Instr (Local_init _)} as s) -> Stmt (kf, s)
+      | _ -> raise Not_found
+    end
   | PLval (kf, ki, _) | PExp (kf, ki, _) | PVDecl (kf, ki, _) ->
     begin
       match kf, ki with

src/plugins/eva/api/values_request.ml

@@ -403,17 +403,17 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
   (* Result of an evaluation: a generic value for scalar types, or an offsetmap
      for struct and arrays. *)
   type result =
-    | Value of A.Val.t
+    | Value of A.Val.t Eval.flagged_value
     | Offsetmap of offsetmap
     | Status of truth
 
   let pp_result typ fmt = function
-    | Value v -> A.Val.pretty fmt v
+    | Value v -> (Eval.Flagged_Value.pretty (A.Val.pretty_typ (Some typ))) fmt v
     | Offsetmap offsm -> pp_offsetmap typ fmt offsm
     | Status truth -> Alarmset.Status.pretty fmt truth
 
   let get_pointed_bases = function
-    | Value v -> get_bases (get_cvalue v)
+    | Value v -> get_bases (Bottom.fold ~bottom:Cvalue.V.bottom get_cvalue v.v)
     | Offsetmap offsm -> get_pointed_bases offsm
     | Status _ -> Base.Hptset.empty
 
@@ -460,13 +460,13 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
   let eval_lval lval state =
     match Cil.(unrollType (typeOfLval lval)) with
     | TInt _ | TEnum _ | TPtr _ | TFloat _ ->
-      A.copy_lvalue state lval >>=. fun value ->
-      value.v >>-: fun v -> Value v
+      A.copy_lvalue state lval >>=: fun value -> Value value
     | _ ->
       lval_to_offsetmap lval state >>=: fun offsm -> Offsetmap offsm
 
   let eval_expr expr state =
-    A.eval_expr state expr >>=: fun value -> Value value
+    A.eval_expr state expr >>=: fun value ->
+    Value { v = `Value value; initialized = true; escaping = false }
 
   let eval_pred eval_point predicate state =
     let result =