diff options
| author | Yannick Moy <moy@adacore.com> | 2023-05-17 15:37:03 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-15 09:59:38 +0200 |
| commit | f185ac2efd79c903e7461e91bceb81f3278aec2e (patch) | |
| tree | c51dc96299543793c264779d7f58ba4172ae34d6 /gcc/ada | |
| parent | 17e45a14a2043ae2117f772945de32d402e10f3f (diff) | |
| download | gcc-f185ac2efd79c903e7461e91bceb81f3278aec2e.zip gcc-f185ac2efd79c903e7461e91bceb81f3278aec2e.tar.gz gcc-f185ac2efd79c903e7461e91bceb81f3278aec2e.tar.bz2 | |
ada: Reject Loop_Entry inside prefix of Loop_Entry
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).
Diffstat (limited to 'gcc/ada')
| -rw-r--r-- | gcc/ada/sem_attr.adb | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index dc06435..7a47abd 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -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 |