Module `API.Statement`Source

analyses at the granularity of a statement, i.e. the results are w.r.t. to the state just before the given statement stmt

val points_to_vars : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  VarSet.t

see Abstract_state.points_to_vars

val points_to_lvals : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  LSet.t

see Abstract_state.points_to_lvals

Sourceval alias_sets_vars : stmt:Frama_c_kernel.Cil_types.stmt -> VarSet.t list

see Abstract_state.alias_sets_vars

Sourceval alias_sets_lvals : stmt:Frama_c_kernel.Cil_types.stmt -> LSet.t list

see Abstract_state.alias_sets_lvals

val alias_vars : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  VarSet.t

see Abstract_state.alias_vars

val aliases : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  LSet.t

val alias_lvals : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  LSet.t

see Abstract_state.alias_lvals

val new_aliases_lvals : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  LSet.t

aliases of the given lval lv created by stmt s

val new_aliases_vars : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  VarSet.t

aliases of the given lval lv created by stmt s

val are_aliased : 
  stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  Frama_c_kernel.Cil_types.lval ->
  bool

Install