module Compute:sig
..end
val get_automaton : annotations:bool ->
Cil_types.kernel_function -> Interpreted_automata.automaton
Build the wto for the given automaton (No memoization, use get_wto
instead)
val build_wto : Interpreted_automata.automaton -> Interpreted_automata.wto
val exit_strategy : Interpreted_automata.graph ->
Interpreted_automata.vertex Wto.component -> Interpreted_automata.wto
val output_to_dot : Pervasives.out_channel ->
?number:[ `Stmt | `Vertex ] ->
?wto:Interpreted_automata.wto -> Interpreted_automata.automaton -> unit
type
wto_index_table
val build_wto_index_table : Interpreted_automata.wto -> wto_index_table
val get_wto_index : wto_index_table ->
Interpreted_automata.vertex -> Interpreted_automata.wto_index
val wto_index_diff : Interpreted_automata.wto_index ->
Interpreted_automata.wto_index ->
Interpreted_automata.vertex list * Interpreted_automata.vertex list
val get_wto_index_diff : wto_index_table ->
Interpreted_automata.vertex ->
Interpreted_automata.vertex ->
Interpreted_automata.vertex list * Interpreted_automata.vertex list
v
is a component head or notval is_wto_head : wto_index_table ->
Interpreted_automata.vertex -> bool
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.val is_back_edge : wto_index_table ->
Interpreted_automata.vertex * Interpreted_automata.vertex -> bool