From: Yannick Moy <moy@adacore.com>
Date: Thu, 5 Jan 2023 09:18:51 +0000 (+0100)
Subject: ada: Allow pragmas Annotate between loop pragmas
X-Git-Tag: basepoints/gcc-15~9312
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c9ed0840840911e3e936f15327acda3f807d7142;p=thirdparty%2Fgcc.git

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 266a433d6c40..6b1f9263f9db 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