API.Abstract_state
Type denothing an abstract state of the analysis. It is a graph containing all aliases and points-to information.
val get_graph : t -> G.t
access to the points-to graph
val pretty : ?debug:bool -> Stdlib.Format.formatter -> t -> unit
pretty printer; debug=true prints the graph, debug = false only prints aliased variables
val print_dot : string -> t -> unit
dot printer; first argument is a file name
val find_vertex : Frama_c_kernel.Cil_types.lval -> t -> G.V.t
finds the vertex corresponding to a lval.
val find_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
same as previous function, but return a set of lval. Cannot raise an exception but may return an empty set if the lval is not in the graph
val find_all_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
similar to the previous functions, but does not only give the equivalence class of lv, but also all lv that are aliases in other vertex of the graph
val points_to_set : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
the set of all lvars to which the given variable may point.
val find_transitive_closure :
Frama_c_kernel.Cil_types.lval ->
t ->
(G.V.t * LSet.t) list
find_aliases, then recursively finds other sets of lvals. We have the property (if lval lv
is in abstract state x
) : List.hd (find_transitive_closure lv x) = (find_vertex lv x, find_aliases lv x)