From: Yannick Moy <m...@adacore.com>
Pragma Annotate is now allowed between loop pragmas, in order to
be able to justify separate loop checks in GNATprove.
gcc/ada/
* sem_prag.adb (Check_Grouping): Allow Annotate pragmas between
loop pragmas.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_prag.adb | 8 ++++++++
1 file changed, 8 insertions(+)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 266a433d6c4..6b1f9263f9d 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -6258,6 +6258,14 @@ package body Sem_Prag is
elsif Is_Loop_Pragma (Stmt) then
Prag := Stmt;
+ -- Skip Annotate pragmas, typically used to justify
+ -- unproved loop pragmas in GNATprove.
+
+ elsif Nkind (Stmt) = N_Pragma
+ and then Pragma_Name (Stmt) = Name_Annotate
+ then
+ null;
+
-- Skip declarations and statements generated by
-- the compiler during expansion. Note that some
-- source statements (e.g. pragma Assert) may have
--
2.40.0
