module Logic_functions:sig
..end
Generate C implementations of user-defined logic functions.
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)
and long g_2(long)
val reset : unit -> unit
val tapp_to_exp : loc:Cil_types.location ->
string ->
Env.t ->
Cil_types.kernel_function ->
Cil_types.term ->
Cil_types.logic_info ->
Typing.number_ty list ->
Cil_types.exp list -> Cil_types.varinfo * Cil_types.exp * Env.t
val add_generated_functions : Cil_types.global list -> Cil_types.global list
val predicate_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
Stdlib.ref
val term_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
Stdlib.ref