[Eva] Requests: fixes evaluation of \result in post-conditions.

src/plugins/eva/api/general_requests.ml

@@ -226,8 +226,10 @@ let marker_evaluation_point = function
   | PTermLval (_, _, prop, _) | PIP prop -> property_evaluation_point prop
   | PType _ -> raise Not_found
 
-let term_lval_to_lval tlval =
-  try Logic_to_c.term_lval_to_lval tlval
+let term_lval_to_lval kf tlval =
+  try
+    let result = Option.bind kf Eva_utils.find_return_var in
+    Logic_to_c.term_lval_to_lval ?result tlval
   with Logic_to_c.No_conversion -> raise Not_found
 
 let print_value fmt loc =
@@ -242,8 +244,8 @@ let print_value fmt loc =
       Results.eval_exp expr
     | PVDecl (_, _, vi) when is_scalar vi.vtype ->
       Results.eval_var vi
-    | PTermLval (_, _, _ip, tlval) ->
-      let lval = term_lval_to_lval tlval in
+    | PTermLval (kf, _, _ip, tlval) ->
+      let lval = term_lval_to_lval kf tlval in
       if is_scalar (Cil.typeOfLval lval)
       then Results.eval_lval lval
       else raise Not_found
@@ -288,8 +290,8 @@ module EvaTaints = struct
       | PLval (_, Kstmt stmt, lval) -> Some (expr_of_lval lval, stmt)
       | PExp (_, Kstmt stmt, expr) -> Some (expr, stmt)
       | PVDecl (_, Kstmt stmt, vi) -> Some (expr_of_lval (Var vi, NoOffset), stmt)
-      | PTermLval (_, Kstmt stmt, _, tlval) ->
-        Some (term_lval_to_lval tlval |> expr_of_lval, stmt)
+      | PTermLval (kf, Kstmt stmt, _, tlval) ->
+        Some (term_lval_to_lval kf tlval |> expr_of_lval, stmt)
       | _ -> None
 
   let of_marker marker =

src/plugins/eva/api/general_requests.mli

@@ -32,3 +32,7 @@ type evaluation_point =
 (* Returns the evaluation point of a marker.
    @raises Not_found if the marker cannot be evaluated. *)
 val marker_evaluation_point: Printer_tag.localizable -> evaluation_point
+
+(* Converts an ACSL lval into a C lval.
+   @raises Not_found if the conversion fails. *)
+val term_lval_to_lval: kernel_function option -> term_lval -> lval

src/plugins/eva/api/values_request.ml

@@ -114,12 +114,6 @@ let probe_property = function
     Ppred (Logic_const.pred_of_id_pred pred)
   | _ -> raise Not_found
 
-let probe_term_lval kf tlval =
-  try
-    let result = Option.bind kf Library_functions.get_retres_vi in
-    Plval (Logic_to_c.term_lval_to_lval ?result tlval)
-  with Logic_to_c.No_conversion -> raise Not_found
-
 let probe_marker = function
   | Printer_tag.PLval (_, _, (Var vi, NoOffset))
   | PVDecl (_, _, vi) when Cil.isFunctionType vi.vtype -> raise Not_found
@@ -127,7 +121,8 @@ let probe_marker = function
   | PExp (_, _, e) -> Pexpr e
   | PStmt (_, s) | PStmtStart (_, s) -> probe_stmt s
   | PVDecl (_, _, v) -> Plval (Var v, NoOffset)
-  | PTermLval (kf, _, _, tlval) -> probe_term_lval kf tlval
+  | PTermLval (kf, _, _, tlval) ->
+    Plval (General_requests.term_lval_to_lval kf tlval)
   | PIP property -> probe_property property
   | _ -> raise Not_found
 
@@ -475,9 +470,16 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
   let eval_expr expr state =
     A.eval_expr state expr >>=: fun value -> Value value
 
-  let eval_pred predicate state =
+  let eval_pred eval_point predicate state =
+    let result =
+      match eval_point with
+      | Initial | Pre _ -> None
+      | Stmt stmt ->
+        let kf = Kernel_function.find_englobing_kf stmt in
+        Eva_utils.find_return_var kf
+    in
     let env =
-      Abstract_domain.{ states = (function _ -> A.Dom.top) ; result = None }
+      Abstract_domain.{ states = (function _ -> A.Dom.top) ; result }
     in
     let truth = A.Dom.evaluate_predicate env state predicate in
     `Value (Status truth), Alarmset.none
@@ -518,7 +520,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
     | Pexpr expr ->
       eval_steps (Cil.typeOf expr) (eval_expr expr) eval_point callstack
     | Ppred pred ->
-      eval_steps Cil.intType (eval_pred pred) eval_point callstack
+      eval_steps Cil.intType (eval_pred eval_point pred) eval_point callstack
 end
 
 let proxy =

src/plugins/eva/utils/eva_utils.ml

@@ -138,6 +138,11 @@ let create_new_var name typ =
 
 let is_const_write_invalid typ = Cil.typeHasQualifier "const" typ
 
+let find_return_var kf =
+  match (Kernel_function.find_return kf).skind with
+  | Return (Some ({enode = Lval ((Var vi, NoOffset))}), _) -> Some vi
+  | _ | exception Kernel_function.No_Statement -> None
+
 (* Find if a postcondition contains [\result] *)
 class postconditions_mention_result = object
   inherit Visitor.frama_c_inplace

src/plugins/eva/utils/eva_utils.mli

@@ -72,6 +72,10 @@ val is_const_write_invalid: typ -> bool
 (** Detect that the type is const, and that option [-global-const] is set. In
     this case, we forbid writing in a l-value that has this type. *)
 
+val find_return_var: kernel_function -> varinfo option
+(** Returns the varinfo returned by the given function.
+    Returns None if the function returns void or has no return statement. *)
+
 val postconditions_mention_result: Cil_types.funspec -> bool
 (** Does the post-conditions of this specification mention [\result]? *)