Frama-C 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.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
val alias_sets_vars : stmt:Frama_c_kernel.Cil_types.stmt -> VarSet.t listsee Abstract_state.alias_sets_vars
val alias_sets_lvals : stmt:Frama_c_kernel.Cil_types.stmt -> LSet.t listsee 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 aliases : stmt:Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.lval -> LSet.tval 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