From 8be82aee33776f37c4c6c7655fd623e65af6f270 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 8 Feb 2021 16:22:41 +0100
Subject: [PATCH] [wp] Clear CFG tables after WP
---
src/plugins/wp/cfgAnnot.ml | 9 +++++++++
src/plugins/wp/cfgAnnot.mli | 6 ++++++
src/plugins/wp/cfgGenerator.ml | 2 ++
src/plugins/wp/cfgInfos.ml | 1 +
src/plugins/wp/cfgInfos.mli | 2 ++
5 files changed, 20 insertions(+)
diff --git a/src/plugins/wp/cfgAnnot.ml b/src/plugins/wp/cfgAnnot.ml
index 5944017b75c..235d65c7ff4 100644
--- a/src/plugins/wp/cfgAnnot.ml
+++ b/src/plugins/wp/cfgAnnot.ml
@@ -374,3 +374,12 @@ module LoopContract = WpContext.StaticGenerator(CodeKey)
let get_loop_contract kf stmt = LoopContract.get (kf,stmt)
(* -------------------------------------------------------------------------- *)
+(* --- Clear Tablesnts --- *)
+(* -------------------------------------------------------------------------- *)
+
+let clear () =
+ CallContract.clear () ;
+ LoopContract.clear () ;
+ CodeAssertions.clear ()
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgAnnot.mli b/src/plugins/wp/cfgAnnot.mli
index 302d1b08ba7..5fe25bdd108 100644
--- a/src/plugins/wp/cfgAnnot.mli
+++ b/src/plugins/wp/cfgAnnot.mli
@@ -93,3 +93,9 @@ val get_precond_at : kernel_function -> stmt -> pred_info -> pred_info
val get_call_contract : kernel_function -> call_contract
(* -------------------------------------------------------------------------- *)
+(* --- Clear Tablesnts --- *)
+(* -------------------------------------------------------------------------- *)
+
+val clear : unit -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgGenerator.ml b/src/plugins/wp/cfgGenerator.ml
index d781ebb00f4..c6872377e71 100644
--- a/src/plugins/wp/cfgGenerator.ml
+++ b/src/plugins/wp/cfgGenerator.ml
@@ -213,6 +213,8 @@ struct
end
(List.rev modes)
) task.modes ;
+ CfgAnnot.clear () ;
+ CfgInfos.clear () ;
!collection
end
diff --git a/src/plugins/wp/cfgInfos.ml b/src/plugins/wp/cfgInfos.ml
index 852fe68b4e3..013e77df4fc 100644
--- a/src/plugins/wp/cfgInfos.ml
+++ b/src/plugins/wp/cfgInfos.ml
@@ -252,5 +252,6 @@ module Generator = WpContext.StaticGenerator(Key)
end)
let get kf ?(bhv=[]) ?(prop=[]) () = Generator.get { kf ; bhv ; prop }
+let clear () = Generator.clear ()
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/cfgInfos.mli b/src/plugins/wp/cfgInfos.mli
index b94ab3471ef..b5420e9ffe8 100644
--- a/src/plugins/wp/cfgInfos.mli
+++ b/src/plugins/wp/cfgInfos.mli
@@ -30,6 +30,8 @@ module Cfg = Interpreted_automata
val get : Kernel_function.t -> ?bhv:string list -> ?prop:string list ->
unit -> t
+val clear : unit -> unit
+
val cfg : t -> Cfg.automaton option
val annots : t -> bool
val doomed : t -> WpPropId.prop_id Bag.t
--
GitLab