SPARK_05 (GNAT Reference Manual)

#### 5.2.16 SPARK_05 ¶

[GNAT] This restriction no longer has any effect and is superseded by SPARK 2014, whose restrictions are checked by the tool GNATprove. To check that a codebase respects SPARK 2014 restrictions, mark the code with pragma or aspect `SPARK_Mode`, and run the tool GNATprove at Stone assurance level, as follows:

    gnatprove -P project.gpr --mode=stone

or equivalently:

    gnatprove -P project.gpr --mode=check_all