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
→ -t→ c
The lvals corresponding to the rightmost vertex are c, b.t, 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
→ ,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
← The aliases of "a" are a,b,d
:
a,b
val find_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
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
← The aliases of "a" are a,b,d,*e
:
a,b
d
to .val find_all_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
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.
val points_to_set : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
all the alias sets of a given state Example: a,b
→ c
← d
← ,f The aliases sets are {a,b,d
, ,f
}
all the alias sets of a given state, including reconstructed lvals Example: a,b
→ c
← d
← ,f The aliases sets are {a,b,d,*e,*f
, ,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.