Interpreted_automata.Graph
Generic control flow graphs
module VTable : FCHashtbl.S with type key = vertex
type wto = vertex Wto.partition
val pretty : t Pretty_utils.formatter
Build a wto for the given automaton. The pref
function is a comparison function used to determine what is the best vertex to use as a Wto component head. See Wto.Make
for more details.
val output_to_dot :
?pp_vertex:V.t Pretty_utils.formatter ->
?pp_edge:E.label Pretty_utils.formatter ->
?wto:wto ->
Stdlib.out_channel ->
t ->
unit
Output the automaton in dot format
val exit_strategy : t -> V.t 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.
module type Domain = sig ... end
Abstract domains
module ForwardAnalysis (D : Domain) : sig ... end
Forward dataflow analysis
module BackwardAnalysis (D : Domain) : sig ... end
Forward dataflow analysis