Type denothing an abstract state of the analysis. It is a graph containing all aliases and points-to information.

access to the points-to graph

set of variables associated with given vertex

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>:

• c: simply refers to a variable associated with the vertex.
• b.t: starting from the second vertex one can follow a field-edge labelled t to come upon the rightmost vertex.
• a->t: Following a pointer edge from the leftmost vertex one obtains *a. Following the t field-edge one arrives at the rightmost vertex, corresponding to ( *a ).t or a->t.

pretty printer; debug=true prints the graph, debug = false only prints aliased variables

dot printer; first argument is a file name

finds the vertex corresponding to a lval.

• raises Not_found

  if such a vertex does not exist

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.

all the variables that are aliases of the given lval:

• variables sharing an equivalence class (or: vertex) with lv
• variables from a neighbouring vertex, i.e. a vertex that shares a successor with the vertex of 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>

Yields all lvals that are an alias of a given lval lv. This includes:

• variables sharing an equivalence class (or: vertex) with lv
• variables from a neighbouring vertex, i.e. a vertex that shares a successor with the vertex of lv.
• lvals reconstructed from the variables from the two previous sets.

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>.

the set of all variables to which the given variable may point.

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>>

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.

inclusion test; is_included a1 a2 tests if, for any lvl present in a1 (associated to a vertex v1), that it is also present in a2 (associated to a vertex v2) and that get_lval_set(succ(v1) is included in get_lval_set(succ(v2))