From 597b4d9c82db5d890c04f8e7ac4fac80757d88ee Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 28 Mar 2024 13:02:09 +0100
Subject: [PATCH] [Eva] In Ivette, shows before/after values on statements with
annotation.
As values might have been reduced by assuming the annotation holds.
---
src/plugins/eva/api/values_request.ml | 35 +++++++++++++--------------
1 file changed, 17 insertions(+), 18 deletions(-)
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 4c308de1704..a6b0d03f404 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -83,15 +83,16 @@ let () = Analysis.register_computation_hook ~on:Computed
(* -------------------------------------------------------------------------- *)
let next_steps = function
- | Initial | Pre _ -> []
+ | Initial | Pre _ -> `None
| Stmt (_, stmt) ->
match stmt.skind with
- | If (cond, _, _, _) -> [ `Then cond ; `Else cond ]
- | Instr (Set _ | Call _ | Local_init _) -> [ `After ]
- | Instr (Asm _ | Code_annot _)
+ | If (cond, _, _, _) -> `Condition (stmt, cond)
+ | Instr (Set _ | Call _ | Local_init _) -> `Effect stmt
+ | Instr _ when Annotations.has_code_annot stmt -> `Effect stmt
+ | Instr (Asm _ | Code_annot _ | Skip _)
| Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| TryCatch _ | TryFinally _ | TryExcept _
- | Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
+ | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> `None
let probe_stmt stmt =
match stmt.skind with
@@ -485,16 +486,16 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
(* --- Evaluates all steps (before/after the statement). ------------------ *)
- let do_next eval state stmt callstack =
- match stmt.skind with
- | If (cond, _, _, _) ->
+ let do_next eval state eval_point callstack =
+ match next_steps eval_point with
+ | `Condition (stmt, cond) ->
let then_state = (A.assume_cond stmt state cond true :> dstate) in
let else_state = (A.assume_cond stmt state cond false :> dstate) in
Cond (eval then_state, eval else_state)
- | Instr (Set _ | Call _ | Local_init _) ->
+ | `Effect stmt ->
let after_state = get_stmt_state ~after:true stmt callstack in
After (eval after_state)
- | _ -> Nothing
+ | `None -> Nothing
let eval_steps typ eval eval_point callstack =
let default value = { value; alarms = []; pointed_vars = []; } in
@@ -506,8 +507,8 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let before = domain_state callstack eval_point in
let here = eval before in
let next =
- match before, eval_point with
- | `Value state, Stmt (_, stmt) -> do_next eval state stmt callstack
+ match before with
+ | `Value state -> do_next eval state eval_point callstack
| _ -> Nothing
in
{ here; next; }
@@ -624,12 +625,10 @@ let () =
| Initial | Pre _ -> ()
| Stmt (_kf, stmt) -> set_stmt rq (Some stmt)
end ;
- let on_steps = function
- | `Here -> ()
- | `Then _ | `Else _ -> set_condition rq true
- | `After -> set_effects rq true
- in
- List.iter on_steps (next_steps eval_point)
+ match next_steps eval_point with
+ | `None -> ()
+ | `Condition _ -> set_condition rq true
+ | `Effect _ -> set_effects rq true
in
Request.register_sig ~package getProbeInfo
~kind:`GET ~name:"getProbeInfo"
--
GitLab