API.Statement
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
val alias_sets_vars : stmt:Frama_c_kernel.Cil_types.stmt -> VarSet.t list
see Abstract_state.alias_sets_vars
val 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 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