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
set of lvals which can be used to refered to the given vertex Example graph: <a> → <b> -t→ <c> The lvals corresponding to the rightmost vertex are <c, b.t, a->t>:
t
to come upon the rightmost vertex.*a
. Following the t
field-edge one arrives at the rightmost vertex, corresponding to ( *a ).t
or a->t
.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 -> v
finds the vertex corresponding to a lval.
val find_vars : Frama_c_kernel.Cil_types.lval -> t -> VarSet.t
val find_synonyms : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
Note: You probably want to use alias_lvals
instead of this function. Combining find_vertex
with get_lval_set
, this function yields all the different ways the vertex containing the given lval can be referred to. Example: <a> → <b,c> If a
points to b
, then the vertex containing b
can be referred to not only by b
but also by c
or *a
. Does not raise an exception but returns an empty set if the lval is not in the graph.
val alias_vars : Frama_c_kernel.Cil_types.lval -> t -> VarSet.t
all the variables that are aliases of the given lval:
lv
lv
.Example: <a,b> → <c> ← <d> ← <e> The aliases of a
are <a,b,d>:
b
shares a vertex with a
d
is in a neighbouring vertex, pointing to c
as does <a,b>val alias_lvals : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
Yields all lvals that are an alias of a given lval lv
. This includes:
lv
lv
.Example: <a,b> → <c> ← <d> ← <e> The aliases of a
are <a,b,d,*e>:
b
shares a vertex with a
d
is in a neighbouring vertex, as it shares a successor with <a,b>*e
is obtained by following backwards the pointer edge from <d> to <e>.val points_to_vars : Frama_c_kernel.Cil_types.lval -> t -> VarSet.t
the set of all variables to which the given variable may point.
val points_to_lvals : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
the set of all lvals to which the given variable may point including reconstructed lvals such as *p, a.t, c->s. For some pointer p it will always include *p.
all the alias sets of a given state Example: <a,b> → <c> ← <d> ← <e,f> The aliases sets are <<a,b,d>, <e,f>>
all the alias sets of a given state, including reconstructed lvals Example: <a,b> → <c> ← <d> ← <e,f> The aliases sets are <<a,b,d,*e,*f>, <e,f>>
val find_transitive_closure :
Frama_c_kernel.Cil_types.lval ->
t ->
(v * LSet.t) list
alias_lvals, 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). Only follows pointer edges, not field edges.