package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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))

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct