From 0f9db74d6b89948242a4aeb16e92e022ad1ae2c4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 28 May 2020 14:16:00 +0200
Subject: [PATCH] [wp] Improves initialization filter
---
src/plugins/wp/Conditions.ml | 19 ++++++++++++++-----
1 file changed, 14 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 8ecd2a69fee..9acc9575ac3 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1592,12 +1592,21 @@ struct
exception Found
let has_init filter pred =
- let rec term_is_init_in_state t s =
- match Mstate.lookup s t with
- | Mlval(_, KInit) | Mchunk(_, KInit) -> raise Found
- | _ -> Lang.F.lc_iter (fun t -> term_is_init_in_state t s) t
+ let visited = ref Tset.empty in
+ let rec term_is_init_in_states states t =
+ let raise_if_is_init t s =
+ match Mstate.lookup s t with
+ | Mlval(_, KInit) | Mchunk(_, KInit) -> raise Found
+ | _ -> ()
+ in
+ if Tset.mem t !visited then ()
+ else begin
+ visited := Tset.add t !visited ;
+ List.iter (raise_if_is_init t) states ;
+ Lang.F.lc_iter (term_is_init_in_states states) t
+ end
in
- try List.iter (term_is_init_in_state (F.e_prop pred)) filter ; false
+ try term_is_init_in_states filter (F.e_prop pred) ; false
with Found -> true
let rec do_filter filter p =
--
GitLab