Aspect SPARK_Mode (GNAT Reference Manual) (original) (raw)

Next: Aspect Subprogram_Variant, Previous: Aspect Simple_Storage_Pool_Type, Up: Implementation Defined Aspects [Contents][Index]

3.56 Aspect SPARK_Mode ¶

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.