[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 37dce8b536759d511e39292e90dc938d356f6e90..8fd40527f0a6fddc32a9e5a133a846930e19cd7d 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2018-05-25  Yannick Moy  <moy@adacore.com>
+
+       * sem_prag.adb (Check_Grouping): Modify test to ignore statements and
+       declarations not coming from source.
+
 2018-05-25  Fedor Rybin  <frybin@adacore.com>
 
        * doc/gnat_ugn/gnat_utility_programs.rst: Document new switch

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index cd46404cf8e04917922be548e63d942ea5673528..85a064d3ef2a79a0f40d2f3addbe1d98fa58c766 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -5979,9 +5979,14 @@ package body Sem_Prag is
                               Prag := Stmt;
 
                            --  Skip declarations and statements generated by
-                           --  the compiler during expansion.
+                           --  the compiler during expansion. Note that some
+                           --  source statements (e.g. pragma Assert) may have
+                           --  been transformed so that they do not appear as
+                           --  coming from source anymore, so we instead look
+                           --  at their Original_Node.
 
-                           elsif not Comes_From_Source (Stmt) then
+                           elsif not Comes_From_Source (Original_Node (Stmt))
+                           then
                               null;
 
                            --  A non-pragma is separating the group from the