diff --git a/ivette/src/frama-c/api/generated/plugins/eva/values/index.ts b/ivette/src/frama-c/api/generated/plugins/eva/values/index.ts
index fdebfbe8d2132f19e9c909b8e325f0206c7dba6a..dde6739568c5020a71df49e33ab133fd6fabc6eb 100644
--- a/ivette/src/frama-c/api/generated/plugins/eva/values/index.ts
+++ b/ivette/src/frama-c/api/generated/plugins/eva/values/index.ts
@@ -192,7 +192,7 @@ export const byEvaluation: Compare.Order<evaluation> =
const getValues_internal: Server.GetRequest<
{ callstack?: callstack, target: marker },
{ v_else?: evaluation, v_then?: evaluation, v_after?: evaluation,
- v_before: evaluation }
+ v_before?: evaluation }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getValues',
@@ -201,7 +201,7 @@ const getValues_internal: Server.GetRequest<
v_else: jEvaluation,
v_then: jEvaluation,
v_after: jEvaluation,
- v_before: jEvaluationSafe,
+ v_before: jEvaluation,
}),
signals: [],
};
@@ -209,7 +209,7 @@ const getValues_internal: Server.GetRequest<
export const getValues: Server.GetRequest<
{ callstack?: callstack, target: marker },
{ v_else?: evaluation, v_then?: evaluation, v_after?: evaluation,
- v_before: evaluation }
+ v_before?: evaluation }
>= getValues_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/eva/cells.ts b/ivette/src/frama-c/plugins/eva/cells.ts
index 22f711b1eb39976a9b35f8b1e1f71cfa86646916..6de74f52a707d4381b7d187dc1ac465192f9a283 100644
--- a/ivette/src/frama-c/plugins/eva/cells.ts
+++ b/ivette/src/frama-c/plugins/eva/cells.ts
@@ -175,7 +175,7 @@ export class ValueCache {
.send(Values.getValues, { target: marker, callstack })
.then((r) => {
newValue.errors = undefined;
- newValue.v_before = r.v_before;
+ if (r.v_before) newValue.v_before = r.v_before;
newValue.v_after = r.v_after;
newValue.v_then = r.v_then;
newValue.v_else = r.v_else;
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index bbbca64de7e26a4bdbc2e13db04f0233ec1b9d2d..83526a8cb55f03d695c0da4d8be7da2998740137 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -46,7 +46,6 @@ let package =
type probe =
| Pexpr of exp * stmt
| Plval of lval * stmt
- | Pnone
type callstack = Value_types.callstack
type truth = Abstract_interp.truth
@@ -94,20 +93,20 @@ let next_steps s =
let probe_stmt s =
match s.skind with
- | Instr (Set(lv,_,_)) -> Plval(lv,s)
- | Instr (Call(Some lr,_,_,_)) -> Plval(lr,s)
- | Instr (Local_init(v,_,_)) -> Plval((Var v,NoOffset),s)
- | Return (Some e,_) | If(e,_,_,_) | Switch(e,_,_,_) -> Pexpr(e,s)
- | _ -> Pnone
+ | 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 probe marker =
let open Printer_tag in
match marker with
- | PLval(_,Kstmt s,l) -> Plval(l,s)
- | PExp(_,Kstmt s,e) -> Pexpr(e,s)
+ | 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) -> Plval((Var v,NoOffset),s)
- | _ -> Pnone
+ | PVDecl(_,Kstmt s,v) -> Some (Plval ((Var v,NoOffset),s))
+ | _ -> None
(* -------------------------------------------------------------------------- *)
(* --- Stmt Ranking --- *)
@@ -461,7 +460,6 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
eval_steps (Cil.typeOfLval lval) (eval_lval lval) stmt callstack
| Pexpr (expr, stmt) ->
eval_steps (Cil.typeOf expr) (eval_expr expr) stmt callstack
- | Pnone -> assert false
end
let proxy =
@@ -486,8 +484,8 @@ let () =
let add stmt = List.fold_right CSet.add (A.callstacks stmt) in
let gather_callstacks cset marker =
match probe marker with
- | Pexpr (_, stmt) | Plval (_, stmt) -> add stmt cset
- | Pnone -> cset
+ | Some (Pexpr (_, stmt) | Plval (_, stmt)) -> add stmt cset
+ | None -> cset
in
let cset = List.fold_left gather_callstacks CSet.empty markers in
Ranking.sort (CSet.elements cset)
@@ -563,9 +561,9 @@ let () =
~descr:(Md.plain "Probe informations")
begin fun rq marker ->
match probe marker with
- | Plval (l, s) -> set_probe rq Printer.pp_lval l s
- | Pexpr (e, s) -> set_probe rq Printer.pp_exp e s
- | Pnone -> ()
+ | 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 -> ()
end
(* -------------------------------------------------------------------------- *)
@@ -611,7 +609,7 @@ let () =
and get_cs = Request.param_opt getValues ~name:"callstack"
~descr:(Md.plain "Callstack to collect (defaults to none)")
(module Jcallstack)
- and set_before = Request.result getValues ~name:"v_before"
+ and set_before = Request.result_opt getValues ~name:"v_before"
~descr:(Md.plain "Domain values before execution")
(module JEvaluation)
and set_after = Request.result_opt getValues ~name:"v_after"
@@ -630,14 +628,17 @@ let () =
begin fun rq () ->
let module A : EvaProxy = (val proxy ()) in
let marker = get_tgt rq and callstack = get_cs rq in
- let domain = A.evaluate (probe marker) callstack in
- set_before rq domain.here;
- match domain.next with
- | After value -> set_after rq (Some value)
- | Cond (v_then, v_else) ->
- set_then rq (Some v_then);
- set_else rq (Some v_else)
- | Nothing -> ()
+ match probe marker with
+ | None -> ()
+ | Some probe ->
+ let domain = A.evaluate probe callstack in
+ set_before rq (Some domain.here);
+ match domain.next with
+ | After value -> set_after rq (Some value)
+ | Cond (v_then, v_else) ->
+ set_then rq (Some v_then);
+ set_else rq (Some v_else)
+ | Nothing -> ()
end
(* -------------------------------------------------------------------------- *)