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

  • deprecated Use Statement.points_to_vars or Statement.points_to_lvals instead!
  • deprecated Use Function.points_to_vars or Function.points_to_lvals instead!
  • deprecated Use Statement.aliases instead!
  • deprecated Use Function.aliases instead!
  • deprecated Use Function.fundec_stmts instead!
  • deprecated Use LSet.fold/Statement.points_to_lvals or VarSet.fold/Statement.points_to_vars instead!
  • deprecated Use LSet.fold and Statement.aliases instead!
  • deprecated Use Statement.new_aliases with LSet.fold instead!
  • deprecated Use LSet.fold/Function.points_to_lvals VarSet.fold/Function.points_to_vars instead!

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!

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.

  • deprecated Use Statement.are_aliased instead!

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, evey pointer arithmetic is simplified to an access to an array