Commit 463e0e0a authored by Julien Signoles's avatar Julien Signoles
Browse files

[Logic_function] reset the memo table

parent 7478457c
......@@ -73,8 +73,9 @@ let arg_typ_from_lty lty = match lty with
definitions. *)
let empty_kf lfs typ =
let li = lfs.lfs_li in
let fname = Functions.RTL.mk_gen_name
(Env.Varname.get ~scope:Env.Global li.l_var_info.lv_name)
let fname =
Functions.RTL.mk_gen_name
(Env.Varname.get ~scope:Env.Global li.l_var_info.lv_name)
in
let is_not_returnable = Cil.isArrayType typ in
let ty_f = if is_not_returnable then Cil.voidType else typ in
......@@ -363,6 +364,8 @@ let find_kfs li =
tbl
[]
let reset () = Memo.reset tbl
(*****************************************************************************)
(****************** Generation of function calls *****************************)
(*****************************************************************************)
......
......@@ -23,8 +23,8 @@
open Cil_types
(** Generate C implementations of user-defined logic functions.
A logic function can have multiple C implementations depending on
the types computed for its arguments.
A logic function can have multiple C implementations depending on
the types computed for its arguments.
Eg: Consider the following definition: [integer g(integer x) = x]
with the following calls: [g(5)] and [g(10*INT_MAX)]
They will respectively generate the C prototypes [int g_1(int)]
......@@ -37,11 +37,13 @@ open Cil_types
val generate: loc:location -> Env.t -> term -> logic_info ->
exp list -> logic_type list -> varinfo * exp * Env.t
(** [generate ~loc env t_app li args_exp args_lty] generates the C function
corresponding to [t_app] and returns the associated call. *)
corresponding to [t_app] and returns the associated call. *)
val do_visit: Cil_types.file -> unit
(** Put declarations and definitions of the generated functions in the AST. *)
val reset: unit -> unit
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
......
......@@ -1023,6 +1023,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
initializer
Misc.reset ();
Logic_functions.reset ();
Literal_strings.reset ();
Global_observer.reset ();
Keep_status.before_translation ();
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment