Module Logic_functions

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 : Cil_types.kernel_function ->
Env.t -> ?eargs:Cil_types.exp list -> Cil_types.term -> Cil_types.exp * Env.t

Translate a Tapp term to an expression. If the optional argument eargs is provided, then these expressions are used as arguments of the fonction.

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