diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml index ccdde09c346db4a71756e62975b6b663765da201..469c5cdbe61413fca9fe24cb5a40da8986f73826 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