[gcc r12-4312] [Ada] Valid postconditions incorrectly rejected.

[gcc r12-4312] [Ada] Valid postconditions incorrectly rejected.

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:939047f542ddbe43a36d755a39ba3b531bb5d8cc

commit r12-4312-g939047f542ddbe43a36d755a39ba3b531bb5d8cc
Author: Steve Baird <baird@adacore.com>
Date:   Thu Sep 30 17:36:38 2021 -0700

    [Ada] Valid postconditions incorrectly rejected.
    
    gcc/ada/
    
            * sem_attr.adb (Analyze_Attribute_Old_Result): Permit an
            attribute reference inside a compiler-generated _Postconditions
            procedure. In this case, Subp_Decl is assigned the declaration
            of the enclosing subprogram.
            * exp_util.adb (Insert_Actions): When climbing up the tree
            looking for an insertion point, do not climb past an
            N_Iterated_Component/Element_Association, since this could
            result in inserting a reference to a loop parameter at a
            location outside of the scope of that loop parameter. On the
            other hand, be careful to preserve existing behavior in the case
            of an N_Component_Association node.

Diff:
---
 gcc/ada/exp_util.adb | 14 ++++++++++++--
 gcc/ada/sem_attr.adb | 18 ++++++++++++++++++
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 2ae3dd3a9f9..0a6837ce992 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -7619,8 +7619,18 @@ package body Exp_Util is
                | N_Iterated_Component_Association
                | N_Iterated_Element_Association
             =>
-               if Nkind (Parent (P)) = N_Aggregate
-                 and then Present (Loop_Actions (P))
+               if Nkind (Parent (P)) in N_Aggregate | N_Delta_Aggregate
+
+                 --  We must not climb up out of an N_Iterated_xxx_Association
+                 --  because the actions might contain references to the loop
+                 --  parameter. But it turns out that setting the Loop_Actions
+                 --  attribute in the case of an N_Component_Association
+                 --  when the attribute was not already set can lead to
+                 --  (as yet not understood) bugboxes (gcc failures that are
+                 --  presumably due to malformed trees). So we don't do that.
+
+                 and then (Nkind (P) /= N_Component_Association
+                            or else Present (Loop_Actions (P)))
                then
                   if Is_Empty_List (Loop_Actions (P)) then
                      Set_Loop_Actions (P, Ins_Actions);
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index 4d69d58d3bc..32c5d3785a6 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -1413,6 +1413,15 @@ package body Sem_Attr is
                return;
             end if;
 
+         --  'Old attribute reference ok in a _Postconditions procedure
+
+         elsif Nkind (Prag) = N_Subprogram_Body
+           and then not Comes_From_Source (Prag)
+           and then Nkind (Corresponding_Spec (Prag)) = N_Defining_Identifier
+           and then Chars (Corresponding_Spec (Prag)) = Name_uPostconditions
+         then
+            null;
+
          --  Otherwise the placement of the attribute is illegal
 
          else
@@ -1424,6 +1433,15 @@ package body Sem_Attr is
 
          if Nkind (Prag) = N_Aspect_Specification then
             Subp_Decl := Parent (Prag);
+         elsif Nkind (Prag) = N_Subprogram_Body then
+            declare
+               Enclosing_Scope : constant Node_Id :=
+                 Scope (Corresponding_Spec (Prag));
+            begin
+               pragma Assert (Postconditions_Proc (Enclosing_Scope)
+                               = Corresponding_Spec (Prag));
+               Subp_Decl := Parent (Parent (Enclosing_Scope));
+            end;
          else
             Subp_Decl := Find_Related_Declaration_Or_Body (Prag);
          end if;