package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct