| commit | 3cc0fae4334466cc8da40e454455b08e83c9e932 | |
| author | Yannick Moy <moy@adacore.com> | |
| Thu, 4 Jul 2019 08:06:45 +0000 (4 08:06 +0000) | ||
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | |
| Thu, 4 Jul 2019 08:06:45 +0000 (4 08:06 +0000) | ||
| tree | cdc8e346dcc58caf75d305776ea0a891da21b318 | treesnapshot (tar.gz zip) |
| parent | e3a79ce3c18fc6e1df6176e506095c7f8bac30ab | commitdiff |
[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
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 | diffblobblamehistory | |
| gcc/ada/sem_prag.adb | diffblobblamehistory | |
| gcc/testsuite/ChangeLog | diffblobblamehistory | |
| gcc/testsuite/gnat.dg/spark3.adb | [new file with mode: 0644] | blob |