Frama-C:
Plug-ins:
Libraries:

Frama-C API - Wto_statement

Specialization of WTO for the CIL statement graph. See the Wto module for more details

A weak topological ordering where nodes are Cil statements

module WTO : Datatype.S with type t = wto

The datatype for statement WTOs

val wto_of_kf : Cil_types.kernel_function -> wto
  • returns

    the computed wto for the given function

type wto_index = Cil_types.stmt list

the position of a statement in a wto given as the list of component heads

module WTOIndex : Datatype.S with type t = wto_index

Datatype for wto_index

val wto_index_of_stmt : Cil_types.stmt -> wto_index
  • returns

    the wto_index for a statement

val wto_index_diff : wto_index -> wto_index -> Cil_types.stmt list * Cil_types.stmt list
  • returns

    the components left and the components entered when going from one index to another

val wto_index_diff_of_stmt : Cil_types.stmt -> Cil_types.stmt -> Cil_types.stmt list * Cil_types.stmt list
  • returns

    the components left and the components entered when going from one stmt to another