Module type Cil2cfg.WeiMaoZouChenInput

module type WeiMaoZouChenInput = sig .. end

type graph 
type node 
type tenv 
val init : graph ->
tenv * node
build a new env from a graph, and also return the entry point of the graph which has to be unique.
val fold_succ : (tenv ->
node -> tenv) ->
tenv ->
node -> tenv
apply the function on the node successors
val eq_nodes : node -> node -> bool
val set_pos : tenv ->
node -> int -> tenv
store the position for the node and also the fact that the node has been seen
val reset_pos : tenv ->
node -> tenv
reset the position (set the position to 0), but should keep the information that the node has been seen already.
val get_pos : tenv -> node -> int
get the previously stored position of the node or 0 if nothing has been stored
val get_pos_if_traversed : tenv ->
node -> int option
get the previously stored position of the node if any, or None if set_pos hasn't been called already for this node.
val set_iloop_header : tenv ->
node ->
node -> tenv
set_iloop_header env b h store h as the innermost loop header for b. Beware that this function can be called several times for the same b with different values of h during the computation. Only the last one will give the correct information.
val get_iloop_header : tenv ->
node -> node option
get the node innermost loop header if any
val add_loop_header : tenv ->
node -> tenv
store the node as a loop header.
val add_irreducible : tenv ->
node -> tenv
store the node as an irreducible loop header.
val add_reentry_edge : tenv ->
node ->
node -> tenv
store the edge between the two nodes (n1, n2) as a reentry edge. n2 is the reentry point which means that it is in a loop, but it is not the loop header, and n1 is not in the loop.