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

[Eva] Improves values request: allows evaluations of function parameters, predicates and term lvals

Closes #1238

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

ivette/src/frama-c/plugins/eva/api/values/index.ts

@@ -122,8 +122,8 @@ export const getStmtInfo: Server.GetRequest<
 
 const getProbeInfo_internal: Server.GetRequest<
   marker,
-  { condition: boolean, effects: boolean, rank: number, stmt?: marker,
-    code?: string, evaluable: boolean }
+  { condition: boolean, effects: boolean, stmt?: marker, code?: string,
+    evaluable: boolean }
   > = {
   kind: Server.RqKind.GET,
   name:   'plugins.eva.values.getProbeInfo',
@@ -131,7 +131,6 @@ const getProbeInfo_internal: Server.GetRequest<
   output: Json.jObject({
             condition: Json.jBoolean,
             effects: Json.jBoolean,
-            rank: Json.jNumber,
             stmt: Json.jOption(jMarker),
             code: Json.jOption(Json.jString),
             evaluable: Json.jBoolean,
@@ -141,8 +140,8 @@ const getProbeInfo_internal: Server.GetRequest<
 /** Probe informations */
 export const getProbeInfo: Server.GetRequest<
   marker,
-  { condition: boolean, effects: boolean, rank: number, stmt?: marker,
-    code?: string, evaluable: boolean }
+  { condition: boolean, effects: boolean, stmt?: marker, code?: string,
+    evaluable: boolean }
   >= getProbeInfo_internal;
 
 /** Evaluation of an expression or lvalue */

ivette/src/frama-c/plugins/eva/valuetable.tsx

@@ -211,19 +211,22 @@ function useProbeCache(): Request<Location, Probe> {
 /* -------------------------------------------------------------------------- */
 
 interface StmtProps {
+  fct?: string;
   stmt?: Ast.marker;
   marker?: Ast.marker;
   short?: boolean;
 }
 
 function Stmt(props: StmtProps): JSX.Element | null {
-  const { stmt, marker, short } = props;
-  const { descr, sloc } = States.useMarker(marker);
-  if (!stmt || !marker) return null;
+  const { fct, stmt, marker, short } = props;
+  const { descr } = States.useMarker(stmt);
+  const { sloc } = States.useMarker(marker);
+  if (!marker || !fct) return null;
   // Location sloc should always be defined for statements.
   const label = short ? `@L${sloc?.line}` : `@${sloc?.base}:${sloc?.line}`;
+  const title = stmt ? descr : "Start of function " + fct;
   const className = 'dome-text-cell eva-stmt';
-  return <span className={className} title={descr}>{label}</span>;
+  return <span className={className} title={title}>{label}</span>;
 }
 
 /* -------------------------------------------------------------------------- */
@@ -290,7 +293,7 @@ async function StackInfos(props: StackInfosProps): Promise<JSX.Element> {
         onDoubleClick={onDoubleClick}
       >
         {caller}
-        <Stmt stmt={stmt} marker={stmt} />
+        <Stmt fct={caller} stmt={stmt} marker={stmt} />
       </Cell>
     );
   };
@@ -386,7 +389,7 @@ function ProbeHeader(props: ProbeHeaderProps): JSX.Element {
         <div className='eva-header-text-overflow'>
           <span className='dome-text-cell' title={code}>{code}</span>
         </div>
-        <Stmt stmt={stmt} marker={target} short={true}/>
+        <Stmt fct={fct} stmt={stmt} marker={target} short={true}/>
       </TableCell>
     </th>
   );
@@ -412,17 +415,22 @@ function ProbeDescr(props: ProbeDescrProps): JSX.Element[] {
   const valuesClass = classes('eva-table-values', 'eva-table-values-center');
   const tableClass = classes('eva-table-descrs', 'eva-table-descr-sticky');
   const cls = classes(valuesClass, tableClass);
-  const title = (s: string): string => `Values ${s} the statement evaluation`;
   const elements: JSX.Element[] = [];
   function push(title: string, children: JSX.Element | string): void {
     elements.push(<td className={cls} title={title}>{children}</td>);
   }
-  if (!probe.effects && !probe.condition)
-    push('Values at the statement', '-');
+  if (!probe.effects && !probe.condition) {
+    if (probe.stmt)
+      push('Values at the statement', '-');
+    else if (probe.fct)
+      push('Values at the start of function ' + probe.fct, '-');
+    else
+      push('Values at the start of the analysis', '-');
+  }
   if (probe.effects || probe.condition)
-    push(title('before'), 'Before');
+    push('Values just before the statement', 'Before');
   if (probe.effects)
-    push(title('after'), 'After');
+    push('Values just after the statement', 'After');
   if (probe.condition) {
     const pushCondition = (s: string): void => {
       const t = `Values after the condition, in the ${s.toLowerCase()} branch`;

src/plugins/eva/api/general_requests.ml

@@ -183,31 +183,81 @@ let () = Request.register ~package
 
 (* ----- Register Eva values information ------------------------------------ *)
 
-let term_lval_to_lval tlval =
-  try Logic_to_c.term_lval_to_lval tlval
+type evaluation_point =
+  | Initial
+  | Pre of kernel_function
+  | Stmt of kernel_function * stmt
+
+let post kf =
+  if Analysis.use_spec_instead_of_definition kf
+  then raise Not_found
+  else
+    try Stmt (kf, Kernel_function.find_return kf)
+    with Kernel_function.No_Statement -> raise Not_found
+
+let request_at = function
+  | Initial -> Results.at_start
+  | Stmt (_, stmt) -> Results.before stmt
+  | Pre kf -> Results.at_start_of kf
+
+let property_evaluation_point = function
+  | Property.IPCodeAnnot { ica_kf = kf; ica_stmt = stmt }
+  | IPPropertyInstance { ii_kf = kf; ii_stmt = stmt } -> Stmt (kf, stmt)
+  | IPPredicate {ip_kf; ip_kind = PKEnsures (_, Normal)} -> post ip_kf
+  | IPPredicate { ip_kf = kf;
+                  ip_kind = PKRequires _ | PKAssumes _ | PKTerminates }
+  | IPAssigns {ias_kf = kf} | IPFrom {if_kf = kf} ->
+    Pre kf
+  | IPPredicate _ | IPComplete _ | IPDisjoint _ | IPDecrease _
+  | IPAxiomatic _ | IPLemma _ | IPTypeInvariant _ | IPGlobalInvariant _
+  | IPOther _ | IPAllocation _ | IPReachable _ | IPExtended _ | IPBehavior _ ->
+    raise Not_found
+
+let marker_evaluation_point = function
+  | Printer_tag.PGlobal _ -> Initial
+  | PStmt (kf, stmt) | PStmtStart (kf, stmt) -> Stmt (kf, stmt)
+  | PLval (kf, ki, _) | PExp (kf, ki, _) | PVDecl (kf, ki, _) ->
+    begin
+      match kf, ki with
+      | Some kf, Kstmt stmt -> Stmt (kf, stmt)
+      | Some kf, Kglobal -> Pre kf
+      | None, Kglobal -> Initial
+      | None, Kstmt _ -> assert false
+    end
+  | PTermLval (_, _, prop, _) | PIP prop -> property_evaluation_point prop
+  | PType _ -> raise Not_found
+
+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 =
   let is_scalar = Cil.isScalarType in
-  let kinstr, eval =
+  let evaluation_point = marker_evaluation_point loc in
+  let request = request_at evaluation_point in
+  let eval =
     match loc with
-    | Printer_tag.PLval (_kf, ki, lval) when is_scalar (Cil.typeOfLval lval) ->
-      ki, Results.eval_lval lval
-    | Printer_tag.PExp (_kf, ki, expr) when is_scalar (Cil.typeOf expr) ->
-      ki, Results.eval_exp expr
-    | PVDecl (_kf, ki, vi) when is_scalar vi.vtype ->
-      ki, Results.eval_var vi
-    | PTermLval (_kf, ki, _ip, tlval) ->
-      let lval = term_lval_to_lval tlval in
-      ki, Results.eval_lval lval
+    | Printer_tag.PLval (_, _, lval) when is_scalar (Cil.typeOfLval lval) ->
+      Results.eval_lval lval
+    | Printer_tag.PExp (_, _, expr) when is_scalar (Cil.typeOf expr) ->
+      Results.eval_exp expr
+    | PVDecl (_, _, vi) when is_scalar vi.vtype ->
+      Results.eval_var vi
+    | 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
     | _ -> raise Not_found
   in
   let pretty = Cvalue.V_Or_Uninitialized.pretty in
   let eval_cvalue at = Results.(eval at |> as_cvalue_or_uninitialized) in
-  let before = eval_cvalue (Results.before_kinstr kinstr) in
-  match kinstr with
-  | Kglobal -> pretty fmt before
-  | Kstmt stmt ->
+  let before = eval_cvalue request in
+  match evaluation_point with
+  | Initial | Pre _ -> pretty fmt before
+  | Stmt (_, stmt) ->
     let after = eval_cvalue (Results.after stmt) in
     if Cvalue.V_Or_Uninitialized.equal before after
     then pretty fmt before
@@ -241,8 +291,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

@@ -21,3 +21,18 @@
 (**************************************************************************)
 
 (** General Eva requests registered in the server. *)
+
+open Cil_types
+
+type evaluation_point =
+  | Initial
+  | Pre of kernel_function
+  | Stmt of kernel_function * stmt
+
+(* Returns the evaluation point of a marker.
+   @raise 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.
+   @raise Not_found if the conversion fails. *)
+val term_lval_to_lval: kernel_function option -> term_lval -> lval

src/plugins/eva/api/values_request.ml

@@ -42,9 +42,12 @@ let package =
     ~title:"Eva Values"
     ()
 
-type probe =
-  | Pexpr of exp * stmt
-  | Plval of lval * stmt
+type term = Pexpr of exp | Plval of lval | Ppred of predicate
+type evaluation_point = General_requests.evaluation_point =
+    Initial | Pre of kernel_function | Stmt of kernel_function * stmt
+
+(* A term and the program point where it should be evaluated. *)
+type probe = term * evaluation_point
 
 type callstack = Value_types.callstack
 type truth = Abstract_interp.truth
@@ -81,32 +84,52 @@ let () = Analysis.register_computation_hook ~on:Computed
 (* --- Marker Utilities                                                   --- *)
 (* -------------------------------------------------------------------------- *)
 
-let next_steps s =
-  match s.skind with
-  | If (cond, _, _, _) -> [ `Then cond ; `Else cond ]
-  | Instr (Set _ | Call _ | Local_init _) -> [ `After ]
-  | Instr (Asm _ | Code_annot _)
-  | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
-  | TryCatch _ | TryFinally _ | TryExcept _
-  | Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
-
-let probe_stmt s =
-  match s.skind with
-  | Instr (Set(lv,_,_)) -> Some (Plval (lv,s))
-  | Instr (Call(Some lr,_,_,_)) -> Some (Plval (lr,s))
-  | Instr (Local_init(v,_,_)) -> Some (Plval ((Var v,NoOffset), s))
-  | Return (Some e,_) | If(e,_,_,_) | Switch(e,_,_,_) -> Some (Pexpr (e,s))
-  | _ -> None
+let next_steps = function
+  | Initial | Pre _ -> []
+  | Stmt (_, stmt) ->
+    match stmt.skind with
+    | If (cond, _, _, _) -> [ `Then cond ; `Else cond ]
+    | Instr (Set _ | Call _ | Local_init _) -> [ `After ]
+    | Instr (Asm _ | Code_annot _)
+    | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
+    | TryCatch _ | TryFinally _ | TryExcept _
+    | Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
+
+let probe_stmt stmt =
+  match stmt.skind with
+  | Instr (Set (lv, _, _))
+  | Instr (Call (Some lv, _, _, _)) -> Plval lv
+  | Instr (Local_init (v, _, _)) -> Plval (Var v, NoOffset)
+  | Return (Some e, _) | If (e, _, _, _) | Switch (e, _, _, _) -> Pexpr e
+  | _ -> raise Not_found
+
+let probe_code_annot = function
+  | AAssert (_, p) | AInvariant (_, true, p) -> Ppred p.tp_statement
+  | _ -> raise Not_found
+
+let probe_property = function
+  | Property.IPCodeAnnot ica -> probe_code_annot ica.ica_ca.annot_content
+  | IPPropertyInstance { ii_pred = Some pred }
+  | IPPredicate {ip_pred = pred} ->
+    Ppred (Logic_const.pred_of_id_pred pred)
+  | _ -> raise Not_found
+
+let probe_marker = function
+  | Printer_tag.PLval (_, _, (Var vi, NoOffset))
+  | PVDecl (_, _, vi) when Cil.isFunctionType vi.vtype -> raise Not_found
+  | PLval (_, _, l) -> Plval l
+  | PExp (_, _, e) -> Pexpr e
+  | PStmt (_, s) | PStmtStart (_, s) -> probe_stmt s
+  | PVDecl (_, _, v) -> Plval (Var v, NoOffset)
+  | PTermLval (kf, _, _, tlval) ->
+    Plval (General_requests.term_lval_to_lval kf tlval)
+  | PIP property -> probe_property property
+  | _ -> raise Not_found
 
 let probe marker =
-  let open Printer_tag in
-  match marker with
-  | PLval (_, _, (Var vi, NoOffset)) when Cil.isFunctionType vi.vtype -> None
-  | PLval(_,Kstmt s,l) -> Some (Plval (l,s))
-  | PExp(_,Kstmt s,e) -> Some (Pexpr (e,s))
-  | PStmt(_,s) | PStmtStart(_,s) -> probe_stmt s
-  | PVDecl(_,Kstmt s,v) -> Some (Plval ((Var v,NoOffset),s))
-  | _ -> None
+  try Some (probe_marker marker,
+            General_requests.marker_evaluation_point marker)
+  with Not_found -> None
 
 (* -------------------------------------------------------------------------- *)
 (* --- Stmt Ranking                                                       --- *)
@@ -329,7 +352,8 @@ let filter_variables bases =
 (* -------------------------------------------------------------------------- *)
 
 module type EvaProxy = sig
-  val callstacks : stmt -> callstack list
+  val kf_callstacks : kernel_function -> callstack list
+  val stmt_callstacks : stmt -> callstack list
   val evaluate : probe -> callstack option -> evaluations
 end
 
@@ -346,20 +370,34 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
     let default = fun _ -> Cvalue.V.top in
     Option.value ~default (A.Val.get Main_values.CVal.key)
 
-  let callstacks stmt =
-    match A.get_stmt_state_by_callstack ~after:false stmt with
+  let callstacks get_state_by_callstack elt =
+    match get_state_by_callstack elt with
     | `Top | `Bottom -> []
-    | `Value states -> CSmap.fold_sorted (fun cs _ wcs -> cs :: wcs) states []
+    | `Value states -> CSmap.fold (fun cs _ acc -> cs :: acc) states []
+
+  let kf_callstacks = callstacks A.get_initial_state_by_callstack
+  let stmt_callstacks = callstacks (A.get_stmt_state_by_callstack ~after:false)
 
-  let dstate ~after stmt = function
-    | None -> (A.get_stmt_state ~after stmt :> dstate)
+  let get_state get_consolidated get_by_callstack arg = function
+    | None -> get_consolidated arg
     | Some cs ->
-      match A.get_stmt_state_by_callstack ~selection:[cs] ~after stmt with
+      match get_by_callstack ?selection:(Some [cs]) arg with
       | (`Top | `Bottom) as res -> res
       | `Value cmap ->
         try `Value (CSmap.find cmap cs)
         with Not_found -> `Bottom
 
+  let get_stmt_state ~after =
+    get_state (A.get_stmt_state ~after) (A.get_stmt_state_by_callstack ~after)
+
+  let get_initial_state =
+    get_state A.get_initial_state A.get_initial_state_by_callstack
+
+  let domain_state callstack = function
+    | Initial -> A.get_global_state ()
+    | Pre kf -> get_initial_state kf callstack
+    | Stmt (_, stmt) -> get_stmt_state ~after:false stmt callstack
+
   (* --- Converts an evaluation [result] into an exported [value]. ---------- *)
 
   (* Result of an evaluation: a generic value for scalar types, or an offsetmap
@@ -367,37 +405,42 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
   type result =
     | Value of A.Val.t
     | Offsetmap of offsetmap
+    | Status of truth
 
   let pp_result typ fmt = function
     | Value v -> A.Val.pretty 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)
     | Offsetmap offsm -> get_pointed_bases offsm
+    | Status _ -> Base.Hptset.empty
 
-  let get_pointed_markers stmt result =
+  let get_pointed_markers eval_point result =
     let bases = get_pointed_bases result in
     let vars = filter_variables bases in
-    let kf =
-      try Some (Kernel_function.find_englobing_kf stmt)
-      with Not_found -> None
+    let kf, kinstr =
+      match eval_point with
+      | Initial -> None, Kglobal
+      | Pre kf -> Some kf, Kglobal
+      | Stmt (kf, stmt) -> Some kf, Kstmt stmt
     in
     let to_marker vi =
       let text = Pretty_utils.to_string Printer.pp_varinfo vi in
-      let marker = Printer_tag.PLval (kf, Kstmt stmt, Cil.var vi) in
+      let marker = Printer_tag.PLval (kf, kinstr, Cil.var vi) in
       text, marker
     in
     List.map to_marker vars
 
   (* Creates an exported [value] from an evaluation result. *)
-  let make_value typ stmt (result, alarms) =
+  let make_value typ eval_point (result, alarms) =
     let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty in
     let f alarm status acc = (status, descr alarm) :: acc in
     let alarms = Alarmset.fold f [] alarms |> List.rev in
     let pretty_eval = Bottom.pretty (pp_result typ) in
     let value = Pretty_utils.to_string pretty_eval result in
-    let pointed_markers = get_pointed_markers stmt in
+    let pointed_markers = get_pointed_markers eval_point in
     let pointed_vars = Bottom.fold ~bottom:[] pointed_markers result in
     { value; alarms; pointed_vars }
 
@@ -425,6 +468,18 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
   let eval_expr expr state =
     A.eval_expr state expr >>=: fun value -> Value value
 
+  let eval_pred eval_point predicate state =
+    let result =
+      match eval_point with
+      | Initial | Pre _ -> None
+      | Stmt (kf, _) -> Eva_utils.find_return_var kf
+    in
+    let env =
+      Abstract_domain.{ states = (function _ -> A.Dom.top) ; result }
+    in
+    let truth = A.Dom.evaluate_predicate env state predicate in
+    `Value (Status truth), Alarmset.none
+
   (* --- Evaluates all steps (before/after the statement). ------------------ *)
 
   let do_next eval state stmt callstack =
@@ -434,32 +489,34 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
       let else_state = (A.assume_cond stmt state cond false :> dstate) in
       Cond (eval then_state, eval else_state)
     | Instr (Set _ | Call _ | Local_init _) ->
-      let after_state = dstate ~after:true stmt callstack in
+      let after_state = get_stmt_state ~after:true stmt callstack in
       After (eval after_state)
     | _ -> Nothing
 
-  let eval_steps typ eval stmt callstack =
+  let eval_steps typ eval eval_point callstack =
     let default value = { value; alarms = []; pointed_vars = []; } in
     let eval = function
       | `Bottom -> default "Unreachable"
       | `Top -> default "No information"
-      | `Value state -> make_value typ stmt (eval state)
+      | `Value state -> make_value typ eval_point (eval state)
     in
-    let before = dstate ~after:false stmt callstack in
+    let before = domain_state callstack eval_point in
     let here = eval before in
     let next =
-      match before with
-      | `Bottom | `Top -> Nothing
-      | `Value state -> do_next eval state stmt callstack
+      match before, eval_point with
+      | `Value state, Stmt (_, stmt) -> do_next eval state stmt callstack
+      | _ -> Nothing
     in
     { here; next; }
 
-  let evaluate p callstack =
-    match p with
-    | Plval (lval, stmt) ->
-      eval_steps (Cil.typeOfLval lval) (eval_lval lval) stmt callstack
-    | Pexpr (expr, stmt) ->
-      eval_steps (Cil.typeOf expr) (eval_expr expr) stmt callstack
+  let evaluate (term, eval_point) callstack =
+    match term with
+    | Plval lval ->
+      eval_steps (Cil.typeOfLval lval) (eval_lval lval) eval_point callstack
+    | Pexpr expr ->
+      eval_steps (Cil.typeOf expr) (eval_expr expr) eval_point callstack
+    | Ppred pred ->
+      eval_steps Cil.intType (eval_pred eval_point pred) eval_point callstack
 end
 
 let proxy =
@@ -481,11 +538,14 @@ let () =
     ~output:(module Jlist(Jcallstack))
     begin fun markers ->
       let module A : EvaProxy = (val proxy ()) in
-      let add stmt = List.fold_right CSet.add (A.callstacks stmt) in
       let gather_callstacks cset marker =
-        match probe marker with
-        | Some (Pexpr (_, stmt) | Plval (_, stmt)) -> add stmt cset
-        | None -> cset
+        let list =
+          match probe marker with
+          | Some (_, Stmt (_, stmt)) -> A.stmt_callstacks stmt
+          | Some (_, Pre kf) -> A.kf_callstacks kf
+          | Some (_, Initial) | None -> []
+        in
+        List.fold_left (fun set elt -> CSet.add elt set) cset list
       in
       let cset = List.fold_left gather_callstacks CSet.empty markers in
       Ranking.sort (CSet.elements cset)
@@ -528,6 +588,11 @@ let () =
 (* --- Request getProbeInfo                                               --- *)
 (* -------------------------------------------------------------------------- *)
 
+let is_reachable = function
+  | Stmt (_, stmt) -> Results.is_reachable stmt
+  | Pre kf -> Results.is_called kf
+  | Initial -> Results.is_reachable_kinstr Kglobal
+
 let () =
   let getProbeInfo = Request.signature ~input:(module Jmarker) () in
   let set_evaluable = Request.result getProbeInfo
@@ -539,9 +604,6 @@ let () =
   and set_stmt = Request.result_opt getProbeInfo
       ~name:"stmt" ~descr:(Md.plain "Probe statement")
       (module Jstmt)
-  and set_rank = Request.result getProbeInfo
-      ~name:"rank" ~descr:(Md.plain "Probe statement rank")
-      ~default:0 (module Jint)
   and set_effects = Request.result getProbeInfo
       ~name:"effects" ~descr:(Md.plain "Effectfull statement")
       ~default:false (module Jbool)
@@ -549,27 +611,30 @@ let () =
       ~name:"condition" ~descr:(Md.plain "Conditional statement")
       ~default:false (module Jbool)
   in
-  let set_probe rq pp p s =
+  let set_probe rq pp p eval_point =
     let computed = Analysis.is_computed () in
-    let reachable = Results.is_reachable s in
+    let reachable = is_reachable eval_point in
     set_evaluable rq (computed && reachable);
-    set_code rq (Some (Pretty_utils.to_string pp p)) ;
-    set_stmt rq (Some s) ;
-    set_rank rq (Ranking.stmt s) ;
+    set_code rq (Some (Pretty_utils.to_string pp p));
+    set_stmt rq (match eval_point with Stmt (_, s) -> Some s | _ -> None);
     let on_steps = function
       | `Here -> ()
       | `Then _ | `Else _ -> set_condition rq true
       | `After -> set_effects rq true
-    in List.iter on_steps (next_steps s)
+    in
+    List.iter on_steps (next_steps eval_point)
   in
   Request.register_sig ~package getProbeInfo
     ~kind:`GET ~name:"getProbeInfo"
     ~descr:(Md.plain "Probe informations")
     begin fun rq marker ->
       match probe marker with
-      | Some (Plval (l, s)) -> set_probe rq Printer.pp_lval l s
-      | Some (Pexpr (e, s)) -> set_probe rq Printer.pp_exp  e s
       | None -> set_evaluable rq false
+      | Some (term, eval_point) ->
+        match term with
+        | Plval l -> set_probe rq Printer.pp_lval l eval_point
+        | Pexpr e -> set_probe rq Printer.pp_exp e eval_point
+        | Ppred p -> set_probe rq Printer.pp_predicate p eval_point
     end
 
 (* -------------------------------------------------------------------------- *)

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]? *)