Frama-C API - Result
Extract the result at the return point of the analysed function (just after the return transfer function)
val before : result -> Cil_types.stmt -> state option
Extract the result obtained for the control point immediately before the given statement
val after : result -> Cil_types.stmt -> state option
Extract the result obtained for the control point immediately after the given statement
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 -> state -> unit) -> 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 iter_stmt_asc : (Cil_types.stmt -> state -> unit) -> result -> unit
Same as iter_stmt
but guarantee that the iteration will always be in the same increasing order of statements sid.
val to_dot_output : (Stdlib.Format.formatter -> state -> unit) -> 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 -> state -> unit) -> 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 : result -> state Vertex.Hashtbl.t
Extract the result as a table from control points to states