From bcd4d8a99c338531d79512d82374049841be8874 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 15 Oct 2024 11:17:47 +0200
Subject: [PATCH] [Eva] Lmap.add_binding does not check if the written value is
bottom.
This case should be processed by the caller if needed.
---
src/kernel_services/abstract_interp/cvalue.ml | 5 +++++
src/kernel_services/abstract_interp/lmap.ml | 19 ++++++++-----------
2 files changed, 13 insertions(+), 11 deletions(-)
diff --git a/src/kernel_services/abstract_interp/cvalue.ml b/src/kernel_services/abstract_interp/cvalue.ml
index 18befa2c68..31d72c55b6 100644
--- a/src/kernel_services/abstract_interp/cvalue.ml
+++ b/src/kernel_services/abstract_interp/cvalue.ml
@@ -1058,6 +1058,11 @@ module Model = struct
let v = find_indeterminate ~conflate_bottom state loc in
V_Or_Uninitialized.get_v v
+ let add_binding ~exact mem loc v =
+ if V_Or_Uninitialized.is_bottom v
+ then bottom
+ else add_binding ~exact mem loc v
+
let add_indeterminate_binding ~exact mem loc v =
add_binding ~exact mem loc v
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 260ec8ebae..55a15a5e78 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -656,17 +656,14 @@ struct
| Map m -> Map (M.add_base_value base ~size v ~size_v m)
let add_binding ~exact m loc v =
- (* TODO: this should depend on bottom being strict. *)
- if V.equal v V.bottom then Bottom
- else
- match m with
- | Top -> Top
- | Bottom -> Bottom
- | Map m ->
- try
- let non_bottom, r = M.add_binding ~exact m loc v in
- if non_bottom then Map r else Bottom
- with M.Result_is_top -> Top
+ match m with
+ | Top -> Top
+ | Bottom -> Bottom
+ | Map m ->
+ try
+ let non_bottom, r = M.add_binding ~exact m loc v in
+ if non_bottom then Map r else Bottom
+ with M.Result_is_top -> Top
let find ?(conflate_bottom=true) m loc =
match m with
--
GitLab