Frama-C API - Function
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.tsee Abstract_state.points_to_vars
val points_to_lvals : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> LSet.tsee Abstract_state.points_to_lvals
val alias_sets_vars : kf:Frama_c_kernel.Cil_types.kernel_function -> VarSet.t listsee Abstract_state.alias_sets_vars
val alias_sets_lvals : kf:Frama_c_kernel.Cil_types.kernel_function -> LSet.t listsee Abstract_state.alias_sets_lvals
val alias_vars : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> VarSet.tsee Abstract_state.alias_vars
val alias_lvals : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> LSet.tsee Abstract_state.alias_lvals
val are_aliased : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> Frama_c_kernel.Cil_types.lval -> boolval fundec_stmts : kf:Frama_c_kernel.Cil_types.kernel_function -> Frama_c_kernel.Cil_types.lval -> (Frama_c_kernel.Cil_types.stmt * LSet.t) listlist of pairs s, e where e is the set of lvals aliased to v after each statement s in function kf.