module StoreMotionOracle1: StoreMotionOracle.Make
(
StoreMotionOracle.StTotal
)
type
btr3 = unit -> St.t * BTL.iblock
type
btr2 = St.s -> btr3
type
btr1 = unit -> St.t * btr2
type
btr0 = St.t -> btr1
type
ibtr3 = unit -> BTL.iblock
type
ibtr2 = St.s -> St.s * ibtr3
type
ibtr1 = unit -> ibtr2
type
ibtr0 = St.t ->
(St.t, St.t) StoreMotionOracle.bblock_exit * ibtr1
type
analyse_node = {
|
mutable an_Delayable : St.t option ; |
|
mutable an_tr1 : btr1 option ; |
|
mutable an_Delayable_exit : St.t option ; |
|
mutable an_tr2 : btr2 ; |
|
mutable an_Used : St.s option ; |
|
mutable an_tr3 : btr3 option ; |
}
type
analyze_result = {
}
val transfer_core : BTL.coq_function ->
BTL.code * BTL_Invariants.gluemap * analyze_result
val print_analysis : Stdlib.out_channel ->
BTL.coq_function * analyze_result -> unit
val transfer : BTL.coq_function -> BTL.code * BTL_Invariants.gluemap