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

finds the vertex corresponding to a lval.

  • raises Not_found

    if such a vertex does not exist

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.

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