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 app_to_exp : adata:Assert.t ->
loc:Cil_types.location ->
?tapp:Cil_types.term ->
Cil_types.kernel_function ->
Env.t ->
?eargs:Cil_types.exp list ->
Cil_types.logic_info ->
Cil_types.term list -> Cil_types.exp * Assert.t * Env.t
Translate a Tapp term or a Papp predicate to an expression. If the optional
argument eargs
is provided, then these expressions are used as arguments
of the fonction. The optional argument tapp
is the term corresponding to
the call, in case we are translating a term
val add_generated_functions : Cil_types.global list -> Cil_types.global list
val predicate_to_exp_ref : (adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref
val term_to_exp_ref : (adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
Stdlib.ref