Next: Aspect Suppress_Debug_Info, Previous: Aspect Simple_Storage_Pool_Type, Up: Implementation Defined Aspects
This aspect is equivalent to pragma SPARK_Mode and
may be specified for either or both of the specification and body
of a subprogram or package.