sig
type state
type result
val fixpoint :
?wto:Interpreted_automata.wto ->
Cil_types.kernel_function ->
Interpreted_automata.DataflowAnalysis.state ->
Interpreted_automata.DataflowAnalysis.result
module Result :
sig
val at_entry :
Interpreted_automata.DataflowAnalysis.result ->
Interpreted_automata.DataflowAnalysis.state option
val at_return :
Interpreted_automata.DataflowAnalysis.result ->
Interpreted_automata.DataflowAnalysis.state option
val before :
Interpreted_automata.DataflowAnalysis.result ->
Cil_types.stmt -> Interpreted_automata.DataflowAnalysis.state option
val after :
Interpreted_automata.DataflowAnalysis.result ->
Cil_types.stmt -> Interpreted_automata.DataflowAnalysis.state option
val iter_vertex :
(Interpreted_automata.vertex ->
Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result -> unit
val iter_stmt :
(Cil_types.stmt ->
Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result -> unit
val to_dot_output :
(Stdlib.Format.formatter ->
Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result ->
Stdlib.out_channel -> unit
val to_dot_file :
(Stdlib.Format.formatter ->
Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result ->
Filepath.Normalized.t -> unit
val as_table :
Interpreted_automata.DataflowAnalysis.result ->
Interpreted_automata.DataflowAnalysis.state
Interpreted_automata.Vertex.Hashtbl.t
end
end