diff --git a/ivette/src/frama-c/plugins/eva/api/values/index.ts b/ivette/src/frama-c/plugins/eva/api/values/index.ts
index 5ca5cfd1828b4a25f14a4309ec6cad166c8fd258..a11bcc87de392480262185ee3a757bafe45b9e0e 100644
--- a/ivette/src/frama-c/plugins/eva/api/values/index.ts
+++ b/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 */
diff --git a/ivette/src/frama-c/plugins/eva/valuetable.tsx b/ivette/src/frama-c/plugins/eva/valuetable.tsx
index 4588949ce59e5fb047bc8c76b742bedac915304a..fb777a26aeeae2a2ce63bdeda2236cfbbf190e50 100644
--- a/ivette/src/frama-c/plugins/eva/valuetable.tsx
+++ b/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`;
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 3c75a9020251e3775500b6531321d49bcabcdb8f..ccdde09c346db4a71756e62975b6b663765da201 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/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 =
diff --git a/src/plugins/eva/api/general_requests.mli b/src/plugins/eva/api/general_requests.mli
index 6472763b7e5187d8703feffb06c7581d7b81282f..7e98550daa190962d7250a23df777bc81c9d9d7a 100644
--- a/src/plugins/eva/api/general_requests.mli
+++ b/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
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index c672982553d0d692ed28822bfcb09146bd3d04bc..7a547dec3522e379e1ef6e2d3de5ef83d35bb237 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/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
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 75d902623d8bce4deb8a0a2bcc8eb28181a5b2c8..7dbc948a1e05968b67aeee3d0ae3c17ccae81c3e 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/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
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index 0903cdabad18fdaa60b3c33e59be36f1a4e93f8a..9297eee8543a6b5fe8203d49bb226f6df42f96d9 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/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]? *)