From bc4719028a0dec8dbecb706da61f2ef552a0149d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 27 Mar 2023 13:29:50 +0200
Subject: [PATCH] [Eva] Values request: also evaluates pre- and post-conditions
of functions.
---
src/plugins/eva/api/values_request.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/plugins/eva/api/values_request.ml b/src/plugins/eva/api/values_request.ml
index 93040df685b..2796bb32d74 100644
--- a/src/plugins/eva/api/values_request.ml
+++ b/src/plugins/eva/api/values_request.ml
@@ -109,7 +109,8 @@ let probe_code_annot = function
let probe_property = function
| Property.IPCodeAnnot ica -> probe_code_annot ica.ica_ca.annot_content
- | IPPropertyInstance { ii_pred = Some pred } ->
+ | IPPropertyInstance { ii_pred = Some pred }
+ | IPPredicate {ip_pred = pred} ->
Ppred (Logic_const.pred_of_id_pred pred)
| _ -> raise Not_found
--
GitLab