module LoopInfo: sig
.. end
To use WeiMaoZouChen algorithm,
we need to define how to interact with our CFG graph
type
node = Cil2cfg.CFG.V.t
type
graph = Cil2cfg.t
type
tenv = {
|
graph : Cil2cfg.t ; |
|
dfsp : int Cil2cfg.Ntbl.t ; |
|
: node Cil2cfg.Ntbl.t ; |
|
: node list ; |
|
irreducible : node list ; |
|
unstruct_coef : int ; |
}
val init : Cil2cfg.t -> tenv * Cil2cfg.CFG.V.t
val eq_nodes : Cil2cfg.CFG.V.t -> Cil2cfg.CFG.V.t -> bool
val set_pos : tenv -> Cil2cfg.Ntbl.key -> int -> tenv
val reset_pos : tenv -> Cil2cfg.Ntbl.key -> tenv
val get_pos : tenv -> Cil2cfg.Ntbl.key -> int
val get_pos_if_traversed : tenv -> Cil2cfg.Ntbl.key -> int option
: tenv ->
Cil2cfg.Ntbl.key -> node -> tenv
: tenv -> Cil2cfg.Ntbl.key -> node option
: tenv -> node -> tenv
val add_irreducible : tenv -> node -> tenv
val add_reentry_edge : 'a -> 'b -> 'c -> 'a
val is_irreducible : tenv -> Cil2cfg.CFG.V.t -> bool
val fold_succ : (tenv -> Cil2cfg.CFG.E.vertex -> tenv) ->
tenv -> Cil2cfg.CFG.vertex -> tenv
val unstructuredness : tenv -> float