Commit 56ce7e4a by Yannick Moy Committed by Pierre-Marie de Rodat

[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
parent 5c737a56
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
......
......@@ -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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment