From 9f38e57287d29090d7e43b4a9fbba3cbd263e5c4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 24 Mar 2023 21:58:56 +0100
Subject: [PATCH] [Eva] In Ivette, fixes the value of function parameters in
the Inspector panel.
Function parameters were wrongly evaluated in the initial state of the
analysis instead of the initial state of the given function.
---
src/plugins/eva/api/general_requests.ml | 28 ++++++++++++++++---------
1 file changed, 18 insertions(+), 10 deletions(-)
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index 3c75a902025..c0a00d85c44 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -189,22 +189,30 @@ let term_lval_to_lval tlval =
let print_value fmt loc =
let is_scalar = Cil.isScalarType in
- let kinstr, eval =
+ let kf, kinstr, 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) ->
+ | Printer_tag.PLval (kf, ki, lval) when is_scalar (Cil.typeOfLval lval) ->
+ kf, ki, Results.eval_lval lval
+ | Printer_tag.PExp (kf, ki, expr) when is_scalar (Cil.typeOf expr) ->
+ kf, ki, Results.eval_exp expr
+ | PVDecl (kf, ki, vi) when is_scalar vi.vtype ->
+ kf, ki, Results.eval_var vi
+ | PTermLval (kf, ki, _ip, tlval) ->
let lval = term_lval_to_lval tlval in
- ki, Results.eval_lval lval
+ if is_scalar (Cil.typeOfLval lval)
+ then kf, ki, 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
+ let request =
+ match kf, kinstr with
+ | _, Kstmt stmt -> Results.before stmt
+ | Some kf, Kglobal -> Results.at_start_of kf
+ | None, Kglobal -> Results.at_start
+ in
+ let before = eval_cvalue request in
match kinstr with
| Kglobal -> pretty fmt before
| Kstmt stmt ->
--
GitLab