Module Impact.Register

val compute_annots : unit -> Frama_c_kernel.Cil_types.stmt list

Compute the impact analysis from the impact annotations in the program. Print and slice the results according to the parameters -impact-print and -impact-slice.

  • returns

    the impacted statements

Compute the impact analysis of the given statement.

  • returns

    the impacted statements

Compute the impact analysis of the given set of PDG nodes, that come from the given function.

  • returns

    the impacted nodes