API.StatementSourceanalyses 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.tsee Abstract_state.points_to_vars
val points_to_lvals :
stmt:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
LSet.tsee Abstract_state.points_to_lvals
see Abstract_state.alias_sets_vars
see Abstract_state.alias_sets_lvals
val alias_vars :
stmt:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
VarSet.tsee Abstract_state.alias_vars
val alias_lvals :
stmt:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
LSet.tsee Abstract_state.alias_lvals
val new_aliases_lvals :
stmt:Frama_c_kernel.Cil_types.stmt ->
Frama_c_kernel.Cil_types.lval ->
LSet.taliases 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.taliases 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