diff options
| -rw-r--r-- | gcc/ada/sem_prag.adb | 8 |
1 files changed, 8 insertions, 0 deletions
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 |