[Ada] Detect misplaced assertions between loop invariants
authorYannick Moy <moy@adacore.com>
Fri, 25 May 2018 09:02:58 +0000 (09:02 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Fri, 25 May 2018 09:02:58 +0000 (09:02 +0000)
commit56ce7e4aa9cfbeb2df1a02a4ae899faaeedb2ab4
tree2d1a4a1d495b556e5f224272e2815dddbd291f6a
parent5c737a562b83361afa576c9aba61a788cf354e62
[Ada] Detect misplaced assertions between loop invariants

Loop invariants and loop variants should all be colocated, as defined in
SPARK RM 5.5.3(8). The code checking that rule was incorrectly accepting
pragma Assert between two loop invariants. Now fixed.

2018-05-25  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_prag.adb (Check_Grouping): Modify test to ignore statements and
declarations not coming from source.

From-SVN: r260715
gcc/ada/ChangeLog
gcc/ada/sem_prag.adb