sig
  type btr3 = unit -> StoreMotionOracle.StTotal.t * BTL.iblock
  type btr2 = StoreMotionOracle.StTotal.s -> btr3
  type btr1 = unit -> StoreMotionOracle.StTotal.t * btr2
  type btr0 = StoreMotionOracle.StTotal.t -> btr1
  type ibtr3 = unit -> BTL.iblock
  type ibtr2 =
      StoreMotionOracle.StTotal.s -> StoreMotionOracle.StTotal.s * ibtr3
  type ibtr1 = unit -> ibtr2
  type ibtr0 =
      StoreMotionOracle.StTotal.t ->
      (StoreMotionOracle.StTotal.t, StoreMotionOracle.StTotal.t)
      StoreMotionOracle.bblock_exit * ibtr1
  type analyse_node =
    StoreMotionOracle.Make(StoreMotionOracle.StTotal).analyse_node = {
    mutable an_Delayable : StoreMotionOracle.StTotal.t option;
    mutable an_tr1 : btr1 option;
    mutable an_Delayable_exit : StoreMotionOracle.StTotal.t option;
    mutable an_tr2 : btr2;
    mutable an_Used : StoreMotionOracle.StTotal.s option;
    mutable an_tr3 : btr3 option;
  }
  type analyze_result =
    StoreMotionOracle.Make(StoreMotionOracle.StTotal).analyze_result = {
    aux_tbl : (StoreMotionOracle.address, Registers.reg) Hashtbl.t;
    an_nds : analyse_node Maps.PTree.t;
    stats : StoreMotionOracle.analyze_stats;
  }
  val transfer_core :
    BTL.coq_function -> BTL.code * BTL_Invariants.gluemap * analyze_result
  val print_analysis :
    out_channel -> BTL.coq_function * analyze_result -> unit
  val transfer : BTL.coq_function -> BTL.code * BTL_Invariants.gluemap
end