This aspect may be specified for procedures and functions with side effects; it can be used to list exceptions that might be propagated by the subprogram with side effects in the context of its precondition, and associate them with a specific postcondition.
For the syntax and semantics of this aspect, see the SPARK 2014 Reference Manual, section 6.1.9.