sig
val to_exp :
loc:Cil_datatype.Location.t ->
Cil_types.kernel_function ->
Env.t ->
Misc.pred_or_term -> Cil_types.logic_label -> Cil_types.exp * Env.t
module Malloc :
sig
val find_all : Cil_types.kernel_function -> Cil_types.stmt list
val remove_all : Cil_types.kernel_function -> unit
end
module Free :
sig
val find_all : Cil_types.kernel_function -> Cil_types.stmt list
val remove_all : Cil_types.kernel_function -> unit
end
val predicate_to_exp_ref :
(Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
Pervasives.ref
val term_to_exp_ref :
(Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
Pervasives.ref
end