From c02eabdaa8761749f2b7c3644dce860b61b9ee81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 24 Feb 2021 17:37:30 +0100
Subject: [PATCH] [wp] removed monotonic-inits for gensets
---
src/plugins/wp/MemVar.ml | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 2776f437fd7..e373bd541e2 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -205,6 +205,7 @@ struct
alloc = ALLOC.create () ;
mem = M.Sigma.create () ;
}
+
let copy s = {
vars = SIGMA.copy s.vars ;
init = INIT.copy s.init ;
@@ -1293,6 +1294,7 @@ struct
let conds = assigned_path KValue [p_sloc] xs [] a b ofs in
List.map (fun p -> Assert p) conds
+ (*
let monotonic_initialized_genset s xs mem x ofs p =
if x.vformal || x.vglob then [Assert p_true]
else
@@ -1307,6 +1309,7 @@ struct
in
let conds = assigned_path KInit [not_p; exact_p] xs [] a b ofs in
List.map (fun p -> Assert p) conds
+ *)
(* -------------------------------------------------------------------------- *)
(* --- Assigned --- *)
@@ -1401,7 +1404,7 @@ struct
let k = Lang.freshvar ~basename:"k" Qed.Logic.Int in
let p = Vset.in_range (e_var k) a b in
let ofs = ofs_shift elt (e_var k) ofs in
- (monotonic_initialized_genset seq [k] m x ofs p) @
+ (* (monotonic_initialized_genset seq [k] m x ofs p) @*)
(assigned_genset seq [k] m x ofs p)
let assigned_descr seq obj xs l p =
@@ -1412,7 +1415,7 @@ struct
| Val((HEAP|CTXT|CARR) as m,x,ofs) ->
M.assigned (mseq_of_seq seq) obj (Sdescr(xs,mloc_of_path m x ofs,p))
| Val((CVAL|CREF) as m,x,ofs) ->
- (monotonic_initialized_genset seq xs m x ofs p) @
+ (* (monotonic_initialized_genset seq xs m x ofs p) @ *)
(assigned_genset seq xs m x ofs p)
let assigned seq obj = function
--
GitLab