projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e3a79ce) | patch
[Ada] SPARK_Mode Off now allowed inside subprogram
authorYannick Moy <moy@adacore.com>
Thu, 4 Jul 2019 08:06:45 +0000 (08:06 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 4 Jul 2019 08:06:45 +0000 (08:06 +0000)
commit3cc0fae4334466cc8da40e454455b08e83c9e932
treecdc8e346dcc58caf75d305776ea0a891da21b318tree
parente3a79ce3c18fc6e1df6176e506095c7f8bac30abcommit | diff
[Ada] SPARK_Mode Off now allowed inside subprogram

The rule on SPARK_Mode have been modified so that it is now possible to
have a subprogram or package declared with SPARK_Mode Off inside a
subprogram.

2019-07-04  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_prag.adb (Check_Library_Level_Entity): Update for new rule
on SPARK_Mode.

gcc/testsuite/

* gnat.dg/spark3.adb: New testcase.

From-SVN: r273064
gcc/ada/ChangeLog diff | blob | history
gcc/ada/sem_prag.adb diff | blob | history
gcc/testsuite/ChangeLog diff | blob | history
gcc/testsuite/gnat.dg/spark3.adb [new file with mode: 0644] blob