diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-04 08:06:45 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-04 08:06:45 +0000 |
| commit | 3cc0fae4334466cc8da40e454455b08e83c9e932 (patch) | |
| tree | cdc8e346dcc58caf75d305776ea0a891da21b318 | |
| parent | e3a79ce3c18fc6e1df6176e506095c7f8bac30ab (diff) | |
| download | gcc-3cc0fae4334466cc8da40e454455b08e83c9e932.zip gcc-3cc0fae4334466cc8da40e454455b08e83c9e932.tar.gz gcc-3cc0fae4334466cc8da40e454455b08e83c9e932.tar.bz2 | |
[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
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 11 | ||||
| -rw-r--r-- | gcc/testsuite/ChangeLog | 4 | ||||
| -rw-r--r-- | gcc/testsuite/gnat.dg/spark3.adb | 20 |
4 files changed, 39 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index e476413..f5c2927 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-04 Yannick Moy <moy@adacore.com> + + * sem_prag.adb (Check_Library_Level_Entity): Update for new rule + on SPARK_Mode. + 2019-07-04 Justin Squirek <squirek@adacore.com> * sem_disp.adb (Check_Controlling_Formals): Obtain the full view diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index b499dbd..d841426 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -23189,7 +23189,16 @@ package body Sem_Prag is -- Start of processing for Check_Library_Level_Entity begin - if not Is_Library_Level_Entity (E) then + -- A SPARK_Mode of On shall only apply to library-level + -- entities, except for those in generic instances, which are + -- ignored (even if the entity gets SPARK_Mode pragma attached + -- in the AST, its effect is not taken into account unless the + -- context already provides SPARK_Mode of On in GNATprove). + + if Get_SPARK_Mode_From_Annotation (N) = On + and then not Is_Library_Level_Entity (E) + and then Instantiation_Location (Sloc (N)) = No_Location + then Error_Msg_Name_1 := Pname; Error_Msg_N (Fix_Error (Msg_1), N); diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index 6873356..3502e68 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,7 @@ +2019-07-04 Yannick Moy <moy@adacore.com> + + * gnat.dg/spark3.adb: New testcase. + 2019-07-04 Justin Squirek <squirek@adacore.com> * gnat.dg/tagged2.adb, gnat.dg/tagged2.ads: New testcase. diff --git a/gcc/testsuite/gnat.dg/spark3.adb b/gcc/testsuite/gnat.dg/spark3.adb new file mode 100644 index 0000000..3c9908a --- /dev/null +++ b/gcc/testsuite/gnat.dg/spark3.adb @@ -0,0 +1,20 @@ +-- { dg-do compile } + +procedure SPARK3 (X : in out Integer) with SPARK_Mode is + + procedure Q (X : in out Integer) with SPARK_Mode => Off is + begin + X := X + 1; + end Q; + + procedure R (X : in out Integer); + + procedure R (X : in out Integer) with SPARK_Mode => Off is + begin + Q (X); + end R; + +begin + R (X); + X := X + 1; +end SPARK3; |