module At_with_lscope: sig
.. end
val to_exp : loc:Cil_datatype.Location.t ->
Cil_types.kernel_function ->
Env.t ->
Lscope.pred_or_term -> Cil_types.logic_label -> Cil_types.exp * Env.t
module Malloc: sig
.. end
module Free: sig
.. end
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