diff --git a/src/plugins/instantiate/instantiator_builder.ml b/src/plugins/instantiate/instantiator_builder.ml index df9028d122de56f183632d9571c2f3e3056ec14c..6b98b3ad9d26c521d5cbb90be41c7c45bed3383f 100644 --- a/src/plugins/instantiate/instantiator_builder.ml +++ b/src/plugins/instantiate/instantiator_builder.ml @@ -46,10 +46,9 @@ module type Instantiator = sig val retype_args: override_key -> exp list -> exp list val get_override: override_key -> fundec val get_kfs: unit -> kernel_function list - val mark_as_computed: ?project:Project.t -> unit -> unit + val clear: unit -> unit end - let build_body caller callee args_generator = let open Extlib in let loc = Cil_datatype.Location.unknown in @@ -68,12 +67,13 @@ let build_body caller callee args_generator = module Make_instantiator (G: Generator_sig) = struct include G module Enabled = Options.NewInstantiator (G) - module Cache = State_builder.Hashtbl (G.Hashtbl) (Cil_datatype.Fundec) - (struct - let size = 5 - let dependencies = [] - let name = "Instantiator." ^ G.function_name - end) + module Cache = struct + let tbl = G.Hashtbl.create 13 + let find = G.Hashtbl.find tbl + let add = G.Hashtbl.add tbl + let fold f = G.Hashtbl.fold f tbl + let clear () = G.Hashtbl.clear tbl + end let make_fundec key = let open Globals.Functions in @@ -113,5 +113,6 @@ module Make_instantiator (G: Generator_sig) = struct let get_kfs () = Cache.fold (fun _ fd l -> Globals.Functions.get fd.svar :: l) [] - let mark_as_computed = Cache.mark_as_computed + let clear () = + Cache.clear () end diff --git a/src/plugins/instantiate/instantiator_builder.mli b/src/plugins/instantiate/instantiator_builder.mli index e2432608275499398adeb83d13636fb8ea7f2146..87c268d2d49824682e3f4e2d0ddfa18cd7d081ba 100644 --- a/src/plugins/instantiate/instantiator_builder.mli +++ b/src/plugins/instantiate/instantiator_builder.mli @@ -123,10 +123,9 @@ module type Instantiator = sig *) val get_kfs: unit -> kernel_function list - (** [mark_as_computed ?project ()] applies the [mark_as_computed] on the - internal table. + (** [clear ()] clears the internal table of the instantiator. *) - val mark_as_computed: ?project:Project.t -> unit -> unit + val clear: unit -> unit end (** Generates a [Instantiator] from a [Generator_sig] adding all necessary stuff for diff --git a/src/plugins/instantiate/tests/plugin/ast_clear.c b/src/plugins/instantiate/tests/plugin/ast_clear.c new file mode 100644 index 0000000000000000000000000000000000000000..d3dfbb6ad2a2fb83924f23cba30589f680d415e9 --- /dev/null +++ b/src/plugins/instantiate/tests/plugin/ast_clear.c @@ -0,0 +1,9 @@ +/* run.config + OPT: -instantiate -then -pp-annot +*/ + +#include <string.h> + +int foo(char* s1, char* s2, size_t len){ + return memcmp(s1, s2, len) ; +} \ No newline at end of file diff --git a/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle b/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..1a8c67bb4f4a92cf3d5a5f39514eb119d0d7c121 --- /dev/null +++ b/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle @@ -0,0 +1,2 @@ +[kernel] Parsing tests/plugin/ast_clear.c (with preprocessing) +[kernel] Parsing tests/plugin/ast_clear.c (with preprocessing) diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml index 28f7a1ca81145cb2e7b414d21a0218b59ec6905f..c1f0f29d170495ca9c3421cf725d8c3d5c7a8d37 100644 --- a/src/plugins/instantiate/transform.ml +++ b/src/plugins/instantiate/transform.ml @@ -29,12 +29,6 @@ let register (module G: Generator_sig) = let module Instantiator = Make_instantiator(G) in Hashtbl.add base G.function_name (module Instantiator) -let mark_as_computed () = - let mark_as_computed _ instantiator = - let module I = (val instantiator: Instantiator) in I.mark_as_computed () - in - Hashtbl.iter mark_as_computed base - let get_kfs () = let get_kfs _ instantiator = let module I = (val instantiator: Instantiator) in @@ -43,6 +37,13 @@ let get_kfs () = in Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base [] +let clear () = + let clear _ instantiator = + let module I = (val instantiator: Instantiator) in + I.clear () + in + Hashtbl.iter clear base + module VISet = Cil_datatype.Varinfo.Hptset class transformer = object(self) @@ -55,7 +56,6 @@ class transformer = object(self) let post f = Ast.mark_as_changed () ; Ast.mark_as_grown () ; - mark_as_computed () ; f in Cil.DoChildrenPost post @@ -158,5 +158,6 @@ let compute_statuses_all_kfs () = List.iter compute_comp_disj_statuses kfs let transform file = + clear () ; Visitor.visitFramacFile (new transformer) file ; compute_statuses_all_kfs ()