From da4f3da9d12c2c654fb4672e83611247b0e0a97d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 15 Oct 2020 09:53:59 +0200
Subject: [PATCH] [wp] Factorize normalization in initialized MemVar
---
src/plugins/wp/MemVar.ml | 11 ++++++-----
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 87b4b38c114..4bd0f123fe2 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1104,12 +1104,13 @@ struct
M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
else
let rec normalize obj = function
- | [] -> [], Extlib.id
- | [Shift(elt, i)] when Ctypes.equal obj elt -> [], F.e_add i
- | f :: ofs -> let l, fn = normalize obj ofs in f :: l, fn
+ | [] -> [], a, b
+ | [Shift(elt, i)] when Ctypes.equal obj elt ->
+ [], F.e_add a i, F.e_add b i
+ | f :: ofs ->
+ let l, a, b = normalize obj ofs in f :: l, a, b
in
- let p, shift = normalize elt p in
- let a = shift a and b = shift b in
+ let p, a, b = normalize elt p in
let in_array = valid_range RW (vobject m x) p (elt, a, b) in
let initialized =
if x.vformal || x.vglob then p_true
--
GitLab