Frama-C:
Plug-ins:
Libraries:

Frama-C API - Table

val build : wto -> t

Compute the index table from a wto

val find : t -> vertex -> wto_index
  • returns

    the wto_index for a statement

val is_head : t -> vertex -> bool
  • returns

    wether v is a component head or not

val is_back_edge : t -> (vertex * vertex) -> bool
  • returns

    wether v1,v2 is a back edge of a loop, i.e. if the vertex v1 is a wto head of any component where v2 is included. This assumes that (v1,v2) is actually an edge present in the control flow graph.