aboutsummaryrefslogtreecommitdiff
path: root/libsanitizer
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2018-05-25 09:02:58 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2018-05-25 09:02:58 +0000
commit56ce7e4aa9cfbeb2df1a02a4ae899faaeedb2ab4 (patch)
tree2d1a4a1d495b556e5f224272e2815dddbd291f6a /libsanitizer
parent5c737a562b83361afa576c9aba61a788cf354e62 (diff)
downloadgcc-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 'libsanitizer')
0 files changed, 0 insertions, 0 deletions