Routine Unit_Declaration_Node now recognizes protected types as program
units and returns their declaration nodes; previously it returned
declaration nodes of the enclosing program units. This was an oversight.
------------
-- Source --
------------
-- illegal.ads
package Illegal
with SPARK_Mode
is
protected type PT
with SPARK_Mode => Off
is
end PT;
end Illegal;
-- illegal.adb
package body Illegal
with SPARK_Mode
is
protected body PT
with SPARK_Mode -- Error
is
end PT;
end Illegal;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c illegal.adb
illegal.adb:5:11: incorrect use of SPARK_Mode
illegal.adb:5:11: value Off was set for SPARK_Mode on "PT" at illegal.ads:5
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-10-09 Piotr Trojanek <troja...@adacore.com>
* sem_aux.adb (Unit_Declaration_Node): Detect protected declarations,
just like other program units listed in Ada RM 10.1(1).
Index: sem_aux.adb
===================================================================
--- sem_aux.adb (revision 253546)
+++ sem_aux.adb (working copy)
@@ -1693,6 +1693,7 @@
and then Nkind (N) /= N_Package_Renaming_Declaration
and then Nkind (N) /= N_Procedure_Instantiation
and then Nkind (N) /= N_Protected_Body
+ and then Nkind (N) /= N_Protected_Type_Declaration
and then Nkind (N) /= N_Subprogram_Declaration
and then Nkind (N) /= N_Subprogram_Body
and then Nkind (N) /= N_Subprogram_Body_Stub
