* [COMMITTED] ada: Allow pragmas Annotate between loop pragmas
@ 2023-05-15 9:42 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-05-15 9:42 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
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 --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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-05-15 9:42 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-05-15 9:42 [COMMITTED] ada: Allow pragmas Annotate between loop pragmas Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).