[wp] Clear CFG tables after WP

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 ()
+
+(* -------------------------------------------------------------------------- *)

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
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/cfgGenerator.ml

@@ -213,6 +213,8 @@ struct
              end
              (List.rev modes)
         ) task.modes ;
+      CfgAnnot.clear () ;
+      CfgInfos.clear () ;
       !collection
     end
 

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 ()
 
 (* -------------------------------------------------------------------------- *)

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