Frama-C:
Plug-ins:
Libraries:

Frama-C API - API

External API of the plugin Alias

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

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.

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.

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

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.

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.

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