Module API.Abstract_state

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