Interpreted_automata.Compute
This module defines the previous functions without memoization
val get_automaton : annotations:bool -> Cil_types.kernel_function -> automaton
Get the interpreted automaton for the given kernel_function. Note that the automata construction may lead to the build of new Cil expressions which will be different at each call: you may need to memoize the results of this function.
Build the wto for the given automaton (No memoization, use get_wto instead)
val exit_strategy : graph -> vertex Wto.component -> wto
Extract an exit strategy from a component, i.e. a sub-wto where all vertices lead outside the wto without passing through the head.
val output_to_dot :
Stdlib.out_channel ->
?labeling:vertex labeling ->
?wto:wto ->
automaton ->
unit
Output the automaton in dot format
val build_wto_index_table : wto -> wto_index_table
Compute the index table from a wto
val get_wto_index : wto_index_table -> vertex -> wto_index
val get_wto_index_diff :
wto_index_table ->
vertex ->
vertex ->
vertex list * vertex list
val is_wto_head : wto_index_table -> vertex -> bool
val is_back_edge : wto_index_table -> (vertex * vertex) -> bool