From 7e4a0e44e2a7b90a121d49d4ef6e060d9d121c33 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 6 Feb 2020 14:29:41 +0100
Subject: [PATCH] [Eva] Eval_terms: fixes evaluation of \initialized and
\dangling on empty sets.
---
src/plugins/value/legacy/eval_terms.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 92bb922726e..370396757e4 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -1596,7 +1596,7 @@ let eval_forall_predicate state r test =
let under_loc = make_loc r.eunder in
forall_in_under_location state under_loc test
| True -> True
- | False -> False
+ | False -> if r.empty then Unknown else False
(* Evaluation of an \initialized predicate on a location evaluated to [r]
in the state [state]. *)
--
GitLab