diff mbox series

[COMMITTED] ada: Allow pragmas Annotate between loop pragmas

Message ID 20230515094229.1407641-1-poulhies@adacore.com
State Accepted
Headers
Series [COMMITTED] ada: Allow pragmas Annotate between loop pragmas |

Checks

Context Check Description
snail/gcc-patch-check success Github commit url

Commit Message

Marc Poulhiès May 15, 2023, 9:42 a.m. UTC 
  From: Yannick Moy <moy@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 mbox series

Patch

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