module Wto_statement: sig
.. end
Weak topological ordering of statements. See "Bourdoncle,
Efficient chaotic iteration strategies with widenings" for a
complete explanation.
type
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