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

set of lvals stored in a vertex

val pretty : ?debug:bool -> 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 -> G.V.t

finds the vertex corresponding to a lval.

  • raises Not_found

    if such a vertex does not exist

val 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

val 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

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

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

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)

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