API (p.frama-c.29.0.doc.frama-c-alias.core.Alias.API)

frama-c
- README
- Library Pdg_types
  - Pdg_types
- Library frama-c-alias.core
  - Alias
    - Analysis
    - API
- Library frama-c-aorai.core
  - Aorai
- Library frama-c-api-generator.core
  - Api_generator
- Library frama-c-callgraph.core
  - Callgraph
- Library frama-c-constant_propagation.core
  - Constant_Propagation
- Library frama-c-dive.core
  - Dive
- Library frama-c-e-acsl.core
  - E_ACSL
- Library frama-c-eva.core
  - Eva
- Library frama-c-eva.gui
  - Eva_gui
- Library frama-c-from.core
  - From
- Library frama-c-from.gui
  - From_gui
- Library frama-c-impact.core
  - Impact
- Library frama-c-impact.gui
  - Impact_gui
- Library frama-c-inout.core
  - Inout
- Library frama-c-instantiate.core
  - Instantiate
- Library frama-c-loop-analysis.core
  - LoopAnalysis
- Library frama-c-markdown-report.core
  - Markdown_report
- Library frama-c-markdown-report.eva-info
- Library frama-c-metrics.core
  - Metrics
- Library frama-c-metrics.gui
  - Metrics_gui
- Library frama-c-nonterm.core
  - Nonterm
- Library frama-c-obfuscator.core
  - Obfuscator
- Library frama-c-occurrence.core
  - Occurrence
- Library frama-c-occurrence.gui
  - Occurrence_gui
- Library frama-c-pdg.core
  - Pdg
- Library frama-c-pdg.types
- Library frama-c-postdominators.core
  - Postdominators
- Library frama-c-reduc.core
  - Reduc
- Library frama-c-report.core
  - Report
- Library frama-c-rtegen.core
  - RteGen
- Library frama-c-rtegen.gui
  - Rtegen_gui
- Library frama-c-scope.core
  - Scope
- Library frama-c-scope.gui
  - Scope_gui
- Library frama-c-security_slicing.core
  - Security_slicing
- Library frama-c-security_slicing.gui
  - Security_slicing_gui
- Library frama-c-server.core
  - Server
- Library frama-c-slicing.core
  - Slicing
- Library frama-c-slicing.gui
  - Slicing_gui
- Library frama-c-sparecode.core
  - Sparecode
- Library frama-c-studia.core
  - Studia
- Library frama-c-studia.gui
  - Studia_gui
- Library frama-c-users.core
  - Users
- Library frama-c-variadic.core
  - Variadic
- Library frama-c-wp.core
  - Wp
- Library frama-c-wp.gui
  - Wp_gui
- Library frama-c.analysis-scripts
  - Analysis_scripts
- Library frama-c.boot
  - Frama_c_boot
- Library frama-c.gui
  - Frama_c_gui
- Library frama-c.init
- Library frama-c.kernel
  - Frama_c_kernel
- Library frama_c_very_first_cmdline
- Library frama_c_very_first_gui
- Library markdown_report_eva_info
  - Markdown_report_eva_info
- Library qed
  - Qed
- Sources

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