From 7ad2c7afe4afad31771a8c9995f96ef60f44bf32 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 2 Dec 2021 18:08:01 +0100
Subject: [PATCH] [Eva] multidim: fix writing overlaping the last bound
---
src/kernel_services/abstract_interp/abstract_memory.ml | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index 7290c7b8cbd..ea1ff820b2e 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -955,7 +955,9 @@ struct
else
match s with
| [] ->
- aux_end start head l (M.smash ~oracle v (M.of_raw m.padding)) uindex []
+ let u = B.upper_bound ~oracle:(fun _ -> oracle) u uindex
+ and v = M.smash ~oracle v (M.of_raw m.padding) in
+ aux_end start head l v u []
| (v',u') :: t ->
(* TODO: do not smash if the slices are covered by the write *)
aux_over start head l (M.smash ~oracle v v') u' t
--
GitLab