ada: Allow pragmas Annotate between loop pragmas

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.

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 266a433d6c407dca7121812cdf3ae690b081460a..6b1f9263f9dba3f4d3ed26c7efe7da03ad2327fb 100644 (file)
--- 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