Frama-C API - `API`

External API of the plugin Alias

module LSet = Frama_c_kernel.Cil_datatype.LvalStructEq.Set

module VarSet = Frama_c_kernel.Cil_datatype.Varinfo.Set

module EdgeLabel : sig ... end

module G : Graph.Sig.G with type V.t = int and type E.label = EdgeLabel.t

type v = G.V.t

val vid : v -> int

module Statement : sig ... end

analyses at the granularity of a statement, i.e. the results are w.r.t. to the state just before the given statement stmt

module Function : sig ... end

analyses at the level of a kernel_function, i.e. the results are w.r.t. to the end of the given function

val points_to_set_stmt : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> LSet.t

deprecated Use Statement.points_to_vars or Statement.points_to_lvals instead!

val points_to_set_kf : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> LSet.t

deprecated Use Function.points_to_vars or Function.points_to_lvals instead!

val aliases_stmt : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> LSet.t

deprecated Use Statement.aliases instead!

val aliases_kf : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> LSet.t

deprecated Use Function.aliases instead!

val fundec_stmts : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> (Frama_c_kernel.Cil_types.stmt * LSet.t) list

deprecated Use Function.fundec_stmts instead!

val fold_points_to_set : ('a -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> 'a

deprecated Use LSet.fold/Statement.points_to_lvals or VarSet.fold/Statement.points_to_vars instead!

val fold_aliases_stmt : ('a -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> 'a

deprecated Use LSet.fold and Statement.aliases instead!

val fold_new_aliases_stmt : ('a -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> 'a

deprecated Use Statement.new_aliases with LSet.fold instead!

val fold_points_to_set_kf : ('a -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> 'a

deprecated Use LSet.fold/Function.points_to_lvals VarSet.fold/Function.points_to_vars instead!

val fold_aliases_kf : ('a -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> 'a

fold_aliases_kf f acc kf lv folds f acc over all the aliases of lval lv at the end of function kf.

deprecated Use LSet.fold/Function.aliases VarSet.fold/alias_vars instead!

val fold_fundec_stmts : ('a -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> 'a

fold_fundec_stmts f acc kf v folds f acc s e on the list of pairs s, e where e is the set of lval aliased to v after statement s in function kf.

val are_aliased : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> Frama_c_kernel.Cil_types.lval -> bool

deprecated Use Statement.are_aliased instead!

val fold_vertex : ('a -> v -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> 'a

fold_vertex f acc kf s v folds f acc i lv to all lv in i, where i is the vertex that represents the equivalence class of v before statement s in function kf.

val fold_vertex_closure : ('a -> v -> Frama_c_kernel.Cil_types.lval -> 'a) -> 'a -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> 'a

fold_vertex_closure f acc kf s v is the transitive closure of function fold_vertex.

direct access to the abstract state. See Abstract_state.mli

module Abstract_state : sig ... end

val get_state_before_stmt : Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.stmt -> Abstract_state.t option

get_state_before_stmt f s gets the abstract state computed after statement s in function f. Returns None if the abstract state is bottom or not computed.

val call_function : Abstract_state.t -> Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval option -> Frama_c_kernel.Cil_types.exp list -> Abstract_state.t option

call_function a f Some(res) args computes the abstract state after the instruction res=f(args) where res is a lval. a is the abstract state before the call. If function f returns no value, use call_function a f None args instead. Returns None if the abstract state a is bottom or not computed.

val simplify_lval : Frama_c_kernel.Cil_types.lval -> Frama_c_kernel.Cil_types.lval

simplify_lval lv returns a lval where every index of an array is replaced by 0, evey pointer arithmetic is simplified to an access to an array

Frama-C API - API

Frama-C API - `API`