[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