Module Cil2cfg.LoopInfo

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;`
	`iloop_header : node Cil2cfg.Ntbl.t;`
	`loop_headers : 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

val set_iloop_header : tenv ->
       Cil2cfg.Ntbl.key -> node -> tenv

val get_iloop_header : tenv -> Cil2cfg.Ntbl.key -> node option

val add_loop_header : 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