sig
  type t
  val empty : Env.t
  val has_no_new_stmt : Env.t -> bool
  type localized_scope =
      LGlobal
    | LFunction of Cil_types.kernel_function
    | LLocal_block of Cil_types.kernel_function
  val new_var :
    loc:Cil_types.location ->
    ?scope:Varname.scope ->
    ?name:string ->
    Env.t ->
    Cil_types.kernel_function ->
    Cil_types.term option ->
    Cil_types.typ ->
    (Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt list) ->
    Cil_types.varinfo * Cil_types.exp * Env.t
  val new_var_and_mpz_init :
    loc:Cil_types.location ->
    ?scope:Varname.scope ->
    ?name:string ->
    Env.t ->
    Cil_types.kernel_function ->
    Cil_types.term option ->
    (Cil_types.varinfo -> Cil_types.exp -> Cil_types.stmt list) ->
    Cil_types.varinfo * Cil_types.exp * Env.t
  module Logic_binding :
    sig
      val add :
        ?ty:Cil_types.typ ->
        Env.t ->
        Cil_types.kernel_function ->
        Cil_types.logic_var -> Cil_types.varinfo * Cil_types.exp * Env.t
      val add_binding :
        Env.t -> Cil_types.logic_var -> Cil_types.varinfo -> Env.t
      val get : Env.t -> Cil_types.logic_var -> Cil_types.varinfo
      val remove : Env.t -> Cil_types.logic_var -> unit
    end
  val add_assert :
    Cil_types.kernel_function ->
    Cil_types.stmt -> Cil_types.predicate -> unit
  val add_stmt :
    ?post:bool ->
    ?before:Cil_types.stmt ->
    Env.t -> Cil_types.kernel_function -> Cil_types.stmt -> Env.t
  val extend_stmt_in_place :
    Env.t ->
    Cil_types.stmt -> label:Cil_types.logic_label -> Cil_types.block -> Env.t
  val push : Env.t -> Env.t
  type where = Before | Middle | After
  val pop_and_get :
    ?split:bool ->
    Env.t ->
    Cil_types.stmt ->
    global_clear:bool -> Env.where -> Cil_types.block * Env.t
  val pop : Env.t -> Env.t
  val transfer : from:Env.t -> Env.t -> Env.t
  val get_generated_variables :
    Env.t -> (Cil_types.varinfo * Env.localized_scope) list
  module Logic_scope :
    sig
      val get : Env.t -> Lscope.t
      val extend : Env.t -> Lscope.lscope_var -> Env.t
      val reset : Env.t -> Env.t
      val set_reset : Env.t -> bool -> Env.t
      val get_reset : Env.t -> bool
    end
  val annotation_kind : Env.t -> Constructor.annotation_kind
  val set_annotation_kind : Env.t -> Constructor.annotation_kind -> Env.t
  val push_loop : Env.t -> Env.t
  val add_loop_invariant : Env.t -> Cil_types.predicate -> Env.t
  val pop_loop : Env.t -> Cil_types.predicate list * Env.t
  val rte : Env.t -> bool -> Env.t
  val generate_rte : Env.t -> bool
  module Context :
    sig val save : Env.t -> unit val restore : Env.t -> Env.t end
  val pretty : Format.formatter -> Env.t -> unit
end