This patch modifies the analysis of aspect/pragma Volatile to correct accept
the annotation when it applies to single protected and single task types, and
SPARK_Mode On is in effect.
------------
-- Source --
------------
-- pack.ads
package Pack with SPARK_Mode is
protected PO_Aspect with Volatile is end; -- OK
protected PO_Pragma is end;
pragma Volatile (PO_Pragma); -- OK
task TO_Aspect with Volatile; -- OK
task TO_Pragma;
pragma Volatile (TO_Pragma); -- OK
end Pack;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c pack.ads
$ gcc -c pack.ads -gnatd.F
cannot generate code for file pack.ads (package spec)
2018-05-28 Hristian Kirtchev <kirtchev@adacore.com>
gcc/ada/
* sem_prag.adb (Process_Atomic_Independent_Shared_Volatile): Include
the declarations of single concurrent types because they fall in the
category of full type and object declarations.
From-SVN: r260820
+2018-05-28 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_prag.adb (Process_Atomic_Independent_Shared_Volatile): Include
+ the declarations of single concurrent types because they fall in the
+ category of full type and object declarations.
+
2018-05-28 Eric Botcazou <ebotcazou@adacore.com>
* repinfo.adb (Compute_Max_Length): Skip _Parent component.
if SPARK_Mode = On
and then Prag_Id = Pragma_Volatile
- and then
- not Nkind_In (Original_Node (Decl), N_Full_Type_Declaration,
- N_Object_Declaration)
+ and then not Nkind_In (Original_Node (Decl),
+ N_Full_Type_Declaration,
+ N_Object_Declaration,
+ N_Single_Protected_Declaration,
+ N_Single_Task_Declaration)
then
Error_Pragma_Arg
("argument of pragma % must denote a full type or object "