procyberian/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

ada: Reject Loop_Entry inside prefix of Loop_Entry

Browse source 
This rule was incompletely stated in SPARK RM and not checked.
This is now fixed.

gcc/ada/

	* sem_attr.adb (Analyze_Attribute): Reject case of Loop_Entry
	inside the prefix of Loop_Entry, as per SPARK RM 5.5.3.1(4,8).
This commit is contained in:
Yannick Moy 2023-05-17 15:37:03 +02:00 • committed by Marc Poulhiès
parent 17e45a14a2
commit f185ac2efd
1 changed files with 18 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
gcc/ada/sem_attr.adb
View file

@ -4784,8 +4784,9 @@ package body Sem_Attr is
Loop_Decl : constant Node_Id := Label_Construct (Parent (Loop_Id));
function Check_Reference (Nod : Node_Id) return Traverse_Result;
-- Determine whether a reference mentions an entity declared
-- within the related loop.
-- Detect attribute 'Loop_Entry in prefix P and determine whether
-- a reference mentions an entity declared within the related
-- loop.
function Declared_Within (Nod : Node_Id) return Boolean;
-- Determine whether Nod appears in the subtree of Loop_Decl but
@ -4796,8 +4797,22 @@ package body Sem_Attr is
---------------------
function Check_Reference (Nod : Node_Id) return Traverse_Result is
Orig_Nod : constant Node_Id := Original_Node (Nod);
-- Check presence of Loop_Entry in the prefix P by looking at
-- the original node for Nod, as it will have been rewritten
-- into its own prefix if the assertion is ignored (see code
-- below).
begin
if Nkind (Nod) = N_Identifier
if Is_Attribute_Loop_Entry (Orig_Nod) then
Error_Msg_Name_1 := Name_Loop_Entry;
Error_Msg_Name_2 := Name_Loop_Entry;
Error_Msg_N
("attribute % cannot appear in the prefix of attribute %",
Nod);
return Abandon;
elsif Nkind (Nod) = N_Identifier
and then Present (Entity (Nod))
and then Declared_Within (Declaration_Node (Entity (Nod)))
then