Module API.FunctionSource

analyses at the level of a kernel_function, i.e. the results are w.r.t. to the end of the given function

see Abstract_state.points_to_vars

see Abstract_state.points_to_lvals

see Abstract_state.alias_sets_vars

Sourceval alias_sets_lvals : kf:Frama_c_kernel.Cil_types.kernel_function -> LSet.t list

see Abstract_state.alias_sets_lvals

see Abstract_state.alias_vars

  • deprecated Use Function.alias_lvals instead!

see Abstract_state.alias_lvals

list of pairs s, e where e is the set of lvals aliased to v after each statement s in function kf.