Fix implementation of SPARK RM 5.5.3.1(5) by accepting objects declared
within the prefix of attribute Loop_Variant itself. This previous code
didn't implement the "... but not within the prefix itself" part of the
rule.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* sem_attr.adb (Declared_Within): Return True for objects
declared within the attribute Loop_Entry prefix itself.diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -4375,7 +4375,8 @@ package body Sem_Attr is
-- within the related loop.
function Declared_Within (Nod : Node_Id) return Boolean;
- -- Determine whether Nod appears in the subtree of Loop_Decl
+ -- Determine whether Nod appears in the subtree of Loop_Decl but
+ -- not within the subtree of the prefix P itself.
---------------------
-- Check_Reference --
@@ -4411,6 +4412,9 @@ package body Sem_Attr is
if Stmt = Loop_Decl then
return True;
+ elsif Stmt = P then
+ return False;
+
-- Prevent the search from going too far
elsif Is_Body_Or_Package_Declaration (Stmt) then
