From c9ed0840840911e3e936f15327acda3f807d7142 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 5 Jan 2023 10:18:51 +0100 Subject: 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. --- gcc/ada/sem_prag.adb | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'gcc/ada') diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 266a433..6b1f926 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 -- cgit v1.1