sig
  type t
  val dummy : Env.t
  val empty : Visitor.frama_c_visitor -> Env.t
  val has_no_new_stmt : Env.t -> bool
  type scope = Global | Function | Local_block
  val new_var :
    loc:Cil_types.location ->
    ?init:bool ->
    ?scope:Env.scope ->
    ?name:string ->
    Env.t ->
    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 ->
    ?init:bool ->
    ?scope:Env.scope ->
    ?name:string ->
    Env.t ->
    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.logic_var -> Cil_types.varinfo * Cil_types.exp * Env.t
      val get : Env.t -> Cil_types.logic_var -> Cil_types.varinfo
      val remove : Env.t -> Cil_types.logic_var -> Env.t
    end
  val add_assert : Env.t -> Cil_types.stmt -> Cil_types.predicate -> unit
  val add_stmt :
    ?init:bool -> ?before:Cil_types.stmt -> Env.t -> Cil_types.stmt -> Env.t
  val extend_stmt_in_place :
    Env.t -> Cil_types.stmt -> pre:bool -> 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.scope) list
  val get_visitor : Env.t -> Visitor.generic_frama_c_visitor
  val get_behavior : Env.t -> Cil.visitor_behavior
  val current_kf : Env.t -> Cil_types.kernel_function option
  val annotation_kind : Env.t -> Misc.annotation_kind
  val set_annotation_kind : Env.t -> Misc.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