Frama-C:
Plug-ins:
Libraries:

Frama-C API - Abstract_state

type t

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 get_vars : v -> t -> VarSet.t

set of variables associated with given vertex

val get_lval_set : v -> t -> LSet.t

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

  • raises Not_found

    if such a vertex does not exist

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.

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
val find_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
  • deprecated Use find_synonyms, alias_vars, or alias_lvals instead!
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:

  • 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 .
val find_all_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t
  • deprecated Use alias_lvals instead!
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
  • deprecated Use points_to_vars or points_to_lvals instead!
val alias_sets_vars : t -> VarSet.t list

all the alias sets of a given state Example: a,b → c ← d ← ,f The aliases sets are {a,b,d, ,f

}

val alias_sets_lvals : t -> LSet.t list

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.

val is_included : t -> t -> bool

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