From a06c4cd58f7aa71ed4b712ed40953d0f43748e9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 28 Mar 2023 11:52:53 +0200
Subject: [PATCH] [Eva] Requests: only evaluates local declarations with
initializer.
---
src/plugins/eva/api/general_requests.ml | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml
index ccdde09c346..469c5cdbe61 100644
--- a/src/plugins/eva/api/general_requests.ml
+++ b/src/plugins/eva/api/general_requests.ml
@@ -216,6 +216,13 @@ let property_evaluation_point = function
let marker_evaluation_point = function
| Printer_tag.PGlobal _ -> Initial
| PStmt (kf, stmt) | PStmtStart (kf, stmt) -> Stmt (kf, stmt)
+ | PVDecl (kf, kinstr, v) when not (v.vformal || v.vglob) ->
+ begin
+ (* Only evaluate declaration of local variable if it is initialized. *)
+ match kf, kinstr with
+ | Some kf, Kstmt ({skind = Instr (Local_init _)} as s) -> Stmt (kf, s)
+ | _ -> raise Not_found
+ end
| PLval (kf, ki, _) | PExp (kf, ki, _) | PVDecl (kf, ki, _) ->
begin
match kf, ki with
--
GitLab