This is the mail archive of the
gcc-patches@gcc.gnu.org
mailing list for the GCC project.
[Ada] Spurious error on aspect Volatile
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Hristian Kirtchev <kirtchev at adacore dot com>
- Date: Mon, 28 May 2018 04:58:14 -0400
- Subject: [Ada] Spurious error on aspect Volatile
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)
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
--- gcc/ada/sem_prag.adb
+++ gcc/ada/sem_prag.adb
@@ -7399,9 +7399,11 @@ package body Sem_Prag is
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 "