diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index ca9395f89d13a37167daff9faef075aca1437b3e..ccdde09c346db4a71756e62975b6b663765da201 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -186,23 +186,23 @@ let () = Request.register ~package
type evaluation_point =
| Initial
| Pre of kernel_function
- | Stmt of stmt
+ | Stmt of kernel_function * stmt
let post kf =
if Analysis.use_spec_instead_of_definition kf
then raise Not_found
else
- try Stmt (Kernel_function.find_return kf)
+ 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
+ | Stmt (_, stmt) -> Results.before stmt
| Pre kf -> Results.at_start_of kf
let property_evaluation_point = function
- | Property.IPCodeAnnot { ica_stmt = stmt }
- | IPPropertyInstance { ii_stmt = stmt } -> Stmt stmt
+ | 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 }
@@ -215,13 +215,14 @@ let property_evaluation_point = function
let marker_evaluation_point = function
| Printer_tag.PGlobal _ -> Initial
- | PStmt (_, stmt) | PStmtStart (_, stmt) -> Stmt stmt
+ | PStmt (kf, stmt) | PStmtStart (kf, stmt) -> Stmt (kf, stmt)
| PLval (kf, ki, _) | PExp (kf, ki, _) | PVDecl (kf, ki, _) ->
begin
match kf, ki with
- | _, Kstmt stmt -> Stmt stmt
+ | 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
@@ -256,7 +257,7 @@ let print_value fmt loc =
let before = eval_cvalue request in
match evaluation_point with
| Initial | Pre _ -> pretty fmt before
- | Stmt stmt ->
+ | Stmt (_, stmt) ->
let after = eval_cvalue (Results.after stmt) in
if Cvalue.V_Or_Uninitialized.equal before after
then pretty fmt before
diff --git a/src/plugins/eva/api/general_requests.mli b/src/plugins/eva/api/general_requests.mli
index 9a1c8699b3d8d81af4a0e23cb8da959610928fb8..d17e8af1caedd4d9451becd876f6aa60c31bcb28 100644
--- a/src/plugins/eva/api/general_requests.mli
+++ b/src/plugins/eva/api/general_requests.mli
@@ -27,7 +27,7 @@ open Cil_types
type evaluation_point =
| Initial
| Pre of kernel_function
- | Stmt of stmt
+ | Stmt of kernel_function * stmt
(* Returns the evaluation point of a marker.
@raises Not_found if the marker cannot be evaluated. *)
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 4fe3f15d5e4d4c257009a42ea17a266cc6101a9d..7a547dec3522e379e1ef6e2d3de5ef83d35bb237 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -44,7 +44,7 @@ let package =
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 stmt
+ 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
@@ -86,7 +86,7 @@ let () = Analysis.register_computation_hook ~on:Computed
let next_steps = function
| Initial | Pre _ -> []
- | Stmt stmt ->
+ | Stmt (_, stmt) ->
match stmt.skind with
| If (cond, _, _, _) -> [ `Then cond ; `Else cond ]
| Instr (Set _ | Call _ | Local_init _) -> [ `After ]
@@ -396,7 +396,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
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
+ | Stmt (_, stmt) -> get_stmt_state ~after:false stmt callstack
(* --- Converts an evaluation [result] into an exported [value]. ---------- *)
@@ -424,9 +424,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
match eval_point with
| Initial -> None, Kglobal
| Pre kf -> Some kf, Kglobal
- | Stmt stmt ->
- let kf = Kernel_function.find_englobing_kf stmt in
- Some kf, Kstmt stmt
+ | Stmt (kf, stmt) -> Some kf, Kstmt stmt
in
let to_marker vi =
let text = Pretty_utils.to_string Printer.pp_varinfo vi in
@@ -474,9 +472,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
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
+ | Stmt (kf, _) -> Eva_utils.find_return_var kf
in
let env =
Abstract_domain.{ states = (function _ -> A.Dom.top) ; result }
@@ -508,7 +504,7 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let here = eval before in
let next =
match before, eval_point with
- | `Value state, Stmt stmt -> do_next eval state stmt callstack
+ | `Value state, Stmt (_, stmt) -> do_next eval state stmt callstack
| _ -> Nothing
in
{ here; next; }
@@ -545,7 +541,7 @@ let () =
let gather_callstacks cset marker =
let list =
match probe marker with
- | Some (_, Stmt stmt) -> A.stmt_callstacks stmt
+ | Some (_, Stmt (_, stmt)) -> A.stmt_callstacks stmt
| Some (_, Pre kf) -> A.kf_callstacks kf
| Some (_, Initial) | None -> []
in
@@ -593,7 +589,7 @@ let () =
(* -------------------------------------------------------------------------- *)
let is_reachable = function
- | Stmt stmt -> Results.is_reachable stmt
+ | Stmt (_, stmt) -> Results.is_reachable stmt
| Pre kf -> Results.is_called kf
| Initial -> Results.is_reachable_kinstr Kglobal
@@ -619,8 +615,8 @@ let () =
let computed = Analysis.is_computed () 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 (match eval_point with Stmt s -> Some s | _ -> None) ;
+ 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