From c2a24d6fba11c68cfad86fc1c61059917a0a25ec Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 27 Feb 2020 14:11:47 +0100
Subject: [PATCH] [Eva] Supports \object_pointer predicate in eval_term.
---
src/plugins/value/legacy/eval_terms.ml | 17 ++++++++++++-----
1 file changed, 12 insertions(+), 5 deletions(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 968ec99416c..995160e3482 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -2143,8 +2143,9 @@ let rec reduce_by_predicate ~alarm_mode env positive p =
reduce_by_valid env positive Write tsets
| _,Pvalid_read (_label,tsets) ->
reduce_by_valid env positive Read tsets
+ | _,Pobject_pointer (_label, tsets) ->
+ reduce_by_valid env positive No_access tsets
- | _,Pobject_pointer (_label, _tsets) -> env (* TODO *)
| _,Pvalid_function _tsets -> env (* TODO *)
| _,(Pinitialized (lbl_initialized,tsets)
@@ -2292,11 +2293,17 @@ and eval_predicate env pred =
ignore (env_state env lbl);
do_eval { env with e_cur = lbl } p
- | Pobject_pointer (_label, _tsets) -> Unknown (* TODO *)
-
- | Pvalid (_label, tsets) | Pvalid_read (_label, tsets) ->
+ | Pvalid (_, tsets)
+ | Pvalid_read (_, tsets)
+ | Pobject_pointer (_, tsets) ->
(* TODO: see same constructor in reduce_by_predicate *)
- let kind = match p.pred_content with Pvalid_read _ -> Read | _ -> Write in
+ let kind =
+ match p.pred_content with
+ | Pvalid_read _ -> Read
+ | Pvalid _ -> Write
+ | Pobject_pointer _ -> No_access
+ | _ -> assert false
+ in
let typ_pointed = Logic_typing.ctype_of_pointed tsets.term_type in
(* Check if we are trying to write in a const l-value *)
if kind = Write && Value_util.is_const_write_invalid typ_pointed
--
GitLab