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