From 07a11d0dea56a62ec46b6724b7e4261a50f397ab Mon Sep 17 00:00:00 2001
From: Virgile Robles <virgile.robles@protonmail.ch>
Date: Tue, 13 Oct 2020 13:47:57 +0200
Subject: [PATCH] [annotations] iter/fold_assigns filter out spurious WriteAnys
---
src/kernel_services/ast_data/annotations.ml | 34 ++++++++++++++++++---
1 file changed, 30 insertions(+), 4 deletions(-)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index dd260448133..2058ae330ee 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -635,11 +635,35 @@ let iter_bhv_gen get iter f kf b =
in
iter_spec_gen get iter f kf
+(* Filter out generic specification. If nothing is
+ * found, call f on generic spec once *)
+let iter_filter_generic to_filter iterator f kf b =
+ let something = ref false in
+ let filter_generic e a =
+ if a <> to_filter then begin something := true; f e a end
+ in iterator filter_generic kf b;
+ if not !something then f Emitter.dummy to_filter
+
+(* Fold version *)
+let fold_filter_generic to_filter iterator f kf b init =
+ let something = ref false in
+ let filter_generic e a acc =
+ if a <> to_filter then (something := true; f e a acc) else acc
+ in let res = iterator filter_generic kf b init in
+ if not !something then f Emitter.dummy to_filter res else res
+
let iter_requires f = iter_bhv_gen (fun b -> b.b_requires) List.iter f
let iter_assumes f = iter_bhv_gen (fun b -> b.b_assumes) List.iter f
let iter_ensures f = iter_bhv_gen (fun b -> b.b_post_cond) List.iter f
-let iter_assigns f = iter_bhv_gen (fun b -> b.b_assigns) (fun f a -> f a) f
-let iter_allocates f = iter_bhv_gen (fun b -> b.b_allocation) (fun f a -> f a) f
+
+let iter_assigns f =
+ iter_filter_generic WritesAny
+ (iter_bhv_gen (fun b -> b.b_assigns) (fun f a -> f a)) f
+
+let iter_allocates f =
+ iter_filter_generic FreeAllocAny
+ (iter_bhv_gen (fun b -> b.b_allocation) (fun f a -> f a)) f
+
let iter_extended f = iter_bhv_gen (fun b -> b.b_extended) List.iter f
let fold_spec_gen get fold f kf acc =
@@ -703,10 +727,12 @@ let fold_ensures f =
(fun f l acc -> List.fold_left (Extlib.swap f) acc l) f
let fold_assigns f =
- fold_bhv_gen (fun b -> b.b_assigns) (fun f a acc -> f a acc) f
+ fold_filter_generic WritesAny
+ (fold_bhv_gen (fun b -> b.b_assigns) (fun f a -> f a)) f
let fold_allocates f =
- fold_bhv_gen (fun b -> b.b_allocation) (fun f a acc -> f a acc) f
+ fold_filter_generic FreeAllocAny
+ (fold_bhv_gen (fun b -> b.b_allocation) (fun f a -> f a)) f
let fold_extended f =
fold_bhv_gen (fun b -> b.b_extended)
--
GitLab