Reset function

src/plugins/e-acsl/exit_points.ml

@@ -46,10 +46,15 @@ let labelled_jumps:
   stmt Stmt.Hashtbl.t = Stmt.Hashtbl.create 17
 (* Map labelled statements back to gotos which lead to them *)
 
-let clear () =
-  Stmt.Hashtbl.clear statement_locals;
-  Stmt.Hashtbl.clear exit_context;
-  Stmt.Hashtbl.clear labelled_jumps
+let reset () =
+  Stmt.Hashtbl.reset statement_locals;
+  Stmt.Hashtbl.reset exit_context;
+  Stmt.Hashtbl.reset labelled_jumps
+
+let empty () =
+  Stmt.Hashtbl.length statement_locals = 0 &&
+    Stmt.Hashtbl.length exit_context = 0 &&
+    Stmt.Hashtbl.length labelled_jumps = 0
 
 let filter_vars varlst1 varlst2 =
   let s1 = Varinfo.Set.of_list varlst1 in
@@ -127,5 +132,5 @@ class jump_context = object (self)
 end
 
 let generate fct =
-  clear ();
+  assert (empty ());
   let _ = Cil.visitCilFunction (new jump_context :> Cil.cilVisitor) fct in ()

src/plugins/e-acsl/exit_points.mli

@@ -31,6 +31,9 @@
 val generate: Cil_types.fundec -> unit
 (** Visit a function and populate data structures used to compute exit points *)
 
+val reset: unit -> unit
+(** Clear all gathered data *)
+
 val delete_vars: Cil_types.stmt -> Cil_types.varinfo list
 (** Given a statement which potentially leads to an early scope exit (such as
    goto, break or continue) return the list of local variables which

src/plugins/e-acsl/visit.ml

@@ -370,19 +370,20 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
     f.sbody.blocals <- blocks
 
   method !vfunc f =
-    Exit_points.generate f;
-    if generate then
+    if generate then begin
+      Exit_points.generate f;
       let kf = Extlib.the self#current_kf in
       Options.feedback ~dkey ~level:2 "entering in function %a."
         Kernel_function.pretty kf;
       List.iter (fun vi -> vi.vghost <- false) f.slocals;
       Cil.DoChildrenPost
         (fun f ->
+          Exit_points.reset ();
           self#add_generated_variables_in_function f;
           Options.feedback ~dkey ~level:2 "function %a done."
             Kernel_function.pretty kf;
           f)
-    else
+    end else
       Cil.DoChildren
 
   method private is_return old_kf stmt =