package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-28.1-Nickel.tar.gz

sha256=0220bc743b7da2468ceb926f331edc7ddfaa7c603ba47962de3e33c8e1e3f593

doc/frama-c-alias.core/Alias/API/Abstract_state/index.html

Module `API.Abstract_state`Source

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_lval_set : G.V.t -> t -> LSet.t

set of lvals stored in a vertex

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 -> G.V.t

finds the vertex corresponding to a lval.

raises Not_found
if such a vertex does not exist

Sourceval find_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t

same as previous function, but return a set of lval. Cannot raise an exception but may return an empty set if the lval is not in the graph

Sourceval find_all_aliases : Frama_c_kernel.Cil_types.lval -> t -> LSet.t

similar to the previous functions, but does not only give the equivalence class of lv, but also all lv that are aliases in other vertex of the graph

Sourceval points_to_set : Frama_c_kernel.Cil_types.lval -> t -> LSet.t

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

Source

val find_transitive_closure : 
  Frama_c_kernel.Cil_types.lval ->
  t ->
  (G.V.t * LSet.t) list

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

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