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