diff mbox series

[Ada] Detect misplaced assertions between loop invariants

Message ID 20180525090605.GA34527@adacore.com
State New
Headers show
Series [Ada] Detect misplaced assertions between loop invariants | expand

Commit Message

Pierre-Marie de Rodat May 25, 2018, 9:06 a.m. UTC 
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.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
diff mbox series

Patch

--- gcc/ada/sem_prag.adb
+++ 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