package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Module `API.Function`Source

analyses at the level of a kernel_function, i.e. the results are w.r.t. to the end of the given function

val points_to_vars : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.lval ->
  VarSet.t

see Abstract_state.points_to_vars

Source

val points_to_lvals : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.lval ->
  LSet.t

see Abstract_state.points_to_lvals

Source

val alias_sets_vars : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  VarSet.t list

see Abstract_state.alias_sets_vars

Source

val alias_sets_lvals : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  LSet.t list

see Abstract_state.alias_sets_lvals

Source

val alias_vars : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.lval ->
  VarSet.t

see Abstract_state.alias_vars

Source

val alias_lvals : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.lval ->
  LSet.t

see Abstract_state.alias_lvals

Source

val are_aliased : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.lval ->
  Frama_c_kernel.Cil_types.lval ->
  bool

Source

val fundec_stmts : 
  kf:Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.lval ->
  (Frama_c_kernel.Cil_types.stmt * LSet.t) list

list of pairs s, e where e is the set of lvals aliased to v after each statement s in function kf.

package frama-c

Module API.FunctionSource

Module `API.Function`Source