package frama-c

  1. Overview
  2. Docs

Module API.Abstract_stateSource

Sourcetype t

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

Sourceval get_graph : t -> G.t

access to the points-to graph

Sourceval get_vars : v -> t -> VarSet.t

set of variables associated with given vertex

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

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.
Sourceval pretty : ?debug:bool -> Format.formatter -> t -> unit

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

Sourceval print_dot : string -> t -> unit

dot printer; first argument is a file name

Sourceval 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

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

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.

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

Sourceval alias_sets_vars : t -> VarSet.t list

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

Sourceval alias_sets_lvals : t -> LSet.t list

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

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

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