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 :
    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 -> 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