diff options
| author | Yannick Moy <moy@adacore.com> | 2018-05-25 09:02:58 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-05-25 09:02:58 +0000 |
| commit | 56ce7e4aa9cfbeb2df1a02a4ae899faaeedb2ab4 (patch) | |
| tree | 2d1a4a1d495b556e5f224272e2815dddbd291f6a /move-if-change | |
| parent | 5c737a562b83361afa576c9aba61a788cf354e62 (diff) | |
| download | gcc-56ce7e4aa9cfbeb2df1a02a4ae899faaeedb2ab4.zip gcc-56ce7e4aa9cfbeb2df1a02a4ae899faaeedb2ab4.tar.gz gcc-56ce7e4aa9cfbeb2df1a02a4ae899faaeedb2ab4.tar.bz2 | |
[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
Diffstat (limited to 'move-if-change')
0 files changed, 0 insertions, 0 deletions