Module Interpreted_automata.Compute

module Compute: sig .. end

This module defines the previous functions without memoization


val get_automaton : annotations:bool ->
Cil_types.kernel_function -> Interpreted_automata.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 build_wto : Interpreted_automata.automaton -> Interpreted_automata.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 exit_strategy : Interpreted_automata.graph ->
Interpreted_automata.vertex Wto.component -> Interpreted_automata.wto

Output the automaton in dot format

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

Compute the index table from a wto

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
val is_wto_head : wto_index_table ->
Interpreted_automata.vertex -> bool
val is_back_edge : wto_index_table ->
Interpreted_automata.vertex * Interpreted_automata.vertex -> bool