sig
val get_automaton :
annotations:bool ->
Cil_types.kernel_function -> Interpreted_automata.automaton
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 :
Stdlib.out_channel ->
?labeling:Interpreted_automata.vertex Interpreted_automata.labeling ->
?wto:Interpreted_automata.wto -> Interpreted_automata.automaton -> unit
type wto_index_table
val build_wto_index_table :
Interpreted_automata.wto -> Interpreted_automata.Compute.wto_index_table
val get_wto_index :
Interpreted_automata.Compute.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 :
Interpreted_automata.Compute.wto_index_table ->
Interpreted_automata.vertex ->
Interpreted_automata.vertex ->
Interpreted_automata.vertex list * Interpreted_automata.vertex list
val is_wto_head :
Interpreted_automata.Compute.wto_index_table ->
Interpreted_automata.vertex -> bool
val is_back_edge :
Interpreted_automata.Compute.wto_index_table ->
Interpreted_automata.vertex * Interpreted_automata.vertex -> bool
end