Module Wto_statement

module Wto_statement: sig .. end
Weak topological ordering of statements. See "Bourdoncle, Efficient chaotic iteration strategies with widenings" for a complete explanation.

type wto = 
| Nil
| Node of Cil_types.stmt * wto
| Component of wto * wto
This type represents a list; Nil is the empty list, Node conses a single element, while Component conses a whole component. Note: Bourdoncle paper always has a single element as the header of a component, and this type does not enforce this.
module WTO: Datatype.S  with type t = wto
wto as Datatype
val depth_of_stmt : Cil_types.stmt -> int
Returns depth of a statement
val wto_of_kf : Cil_types.kernel_function -> wto
Returns wto of a kernel function