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