module Result:sig
..end
val at_entry : Interpreted_automata.DataflowAnalysis.result ->
Interpreted_automata.DataflowAnalysis.state option
Extract the result at the entry point of the analysed function
val at_return : Interpreted_automata.DataflowAnalysis.result ->
Interpreted_automata.DataflowAnalysis.state option
Extract the result at the return point of the analysed function (just after the return transfer function)
val before : Interpreted_automata.DataflowAnalysis.result ->
Cil_types.stmt -> Interpreted_automata.DataflowAnalysis.state option
Extract the result obtained for the control point immediately before the given statement
val after : Interpreted_automata.DataflowAnalysis.result ->
Cil_types.stmt -> Interpreted_automata.DataflowAnalysis.state option
Extract the result obtained for the control point immediately after the given statement
val iter_vertex : (Interpreted_automata.vertex ->
Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result -> unit
Iter on the results obtained at each vertex of the graph. Do nothing when the vertex is not reachable (for instance if transfer returned None)
val iter_stmt : (Cil_types.stmt -> Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result -> unit
Iter on the results obtained before each statements of the function. Do nothing when the vertex is not reachable (for instance if transfer returned None)
val to_dot_output : (Stdlib.Format.formatter ->
Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result -> Stdlib.out_channel -> unit
Output result to the given channel. Must be supplied with a pretty printer for abstract values
val to_dot_file : (Stdlib.Format.formatter ->
Interpreted_automata.DataflowAnalysis.state -> unit) ->
Interpreted_automata.DataflowAnalysis.result -> Filepath.Normalized.t -> unit
Output result to a file with the given path. Must be supplied with pretty printer for abstract values
val as_table : Interpreted_automata.DataflowAnalysis.result ->
Interpreted_automata.DataflowAnalysis.state
Interpreted_automata.Vertex.Hashtbl.t
Extract the result as a table from control points to states