r260715 - in /trunk/gcc/ada: ChangeLog sem_prag...

[pmderodat@gcc.gnu.org]

Author: pmderodat
Date: Fri May 25 09:02:58 2018
New Revision: 260715

URL: https://gcc.gnu.org/viewcvs?rev=260715&root=gcc&view=rev
Log:
[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.

Modified:
    trunk/gcc/ada/ChangeLog
    trunk/gcc/ada/sem_prag.adb