From 56ce7e4aa9cfbeb2df1a02a4ae899faaeedb2ab4 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 25 May 2018 09:02:58 +0000 Subject: [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 gcc/ada/ * sem_prag.adb (Check_Grouping): Modify test to ignore statements and declarations not coming from source. From-SVN: r260715 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_prag.adb | 9 +++++++-- 2 files changed, 12 insertions(+), 2 deletions(-) (limited to 'gcc') diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 37dce8b..8fd4052 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2018-05-25 Yannick Moy + + * sem_prag.adb (Check_Grouping): Modify test to ignore statements and + declarations not coming from source. + 2018-05-25 Fedor Rybin * 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 cd46404..85a064d 100644 --- 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 -- cgit v1.1