package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-alias.core/Alias/API/index.html

Module `Alias.API`Source

External API of the plugin Alias

module LSet = Frama_c_kernel.Cil_datatype.LvalStructEq.Set

module VarSet = Frama_c_kernel.Cil_datatype.Varinfo.Set

Sourcemodule EdgeLabel : sig ... end

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

Sourcetype v = G.V.t

Sourceval vid : v -> int

Sourcemodule 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

Sourcemodule 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

Source

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!

Source

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!

Source

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!

Source

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

deprecated Use Function.aliases instead!

Source

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!

Source

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!

Source

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!

Source

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!

Source

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!

Source

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!

Source

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.

Source

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!

Source

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.

Source

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

Sourcemodule Abstract_state : sig ... end

Source

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.

Source

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.

Source

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

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-alias.core/Alias/API/index.html

Module Alias.APISource

Module `Alias.API`Source