sig
  val for_stmt :
    Env.t -> Cil_types.kernel_function -> Cil_types.stmt -> Env.t
  val to_exp :
    loc:Cil_types.location ->
    adata:Assert.t ->
    Cil_types.kernel_function ->
    Env.t ->
    Analyses_types.pred_or_term ->
    Cil_types.logic_label -> Cil_types.exp * Assert.t * Env.t
  val reset : unit -> unit
  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 term_to_exp_ref :
    (adata:Assert.t ->
     ?inplace:bool ->
     Cil_types.kernel_function ->
     Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref
  val predicate_to_exp_ref :
    (adata:Assert.t ->
     ?inplace:bool ->
     ?name:string ->
     Cil_types.kernel_function ->
     ?rte:bool ->
     Env.t -> Cil_types.predicate -> Cil_types.exp * Assert.t * Env.t)
    Stdlib.ref
end