diff options
| author | Yannick Moy <moy@adacore.com> | 2023-01-05 10:18:51 +0100 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-05-15 11:36:41 +0200 |
| commit | c9ed0840840911e3e936f15327acda3f807d7142 (patch) | |
| tree | 47aa98ff46723c3b3a96cc23c8430b0391df1287 /gcc/ada | |
| parent | b7d26cb1fe3e8f8b44ae82894750d18d2094234e (diff) | |
| download | gcc-c9ed0840840911e3e936f15327acda3f807d7142.zip gcc-c9ed0840840911e3e936f15327acda3f807d7142.tar.gz gcc-c9ed0840840911e3e936f15327acda3f807d7142.tar.bz2 | |
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.
Diffstat (limited to 'gcc/ada')
| -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 |