From 18768a6ac1e0e974935849f217464696dd2e2789 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 22 Feb 2017 17:18:38 +0100
Subject: [PATCH] Reset function
---
src/plugins/e-acsl/exit_points.ml | 15 ++++++++++-----
src/plugins/e-acsl/exit_points.mli | 3 +++
src/plugins/e-acsl/visit.ml | 7 ++++---
3 files changed, 17 insertions(+), 8 deletions(-)
diff --git a/src/plugins/e-acsl/exit_points.ml b/src/plugins/e-acsl/exit_points.ml
index 3ca629adc5a..0833c5c514e 100644
--- a/src/plugins/e-acsl/exit_points.ml
+++ b/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 ()
diff --git a/src/plugins/e-acsl/exit_points.mli b/src/plugins/e-acsl/exit_points.mli
index ea22508bf9c..147b4efccbc 100644
--- a/src/plugins/e-acsl/exit_points.mli
+++ b/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
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 36f07a9f819..539d6ca2d4d 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/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 =
--
GitLab