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 → -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 → ,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 ← 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

• deprecated Use find_synonyms, alias_vars, or alias_lvals instead!

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

• deprecated Use alias_lvals instead!

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.

• deprecated Use points_to_vars or points_to_lvals instead!

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

}

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