[multiple changes]

2015-03-04  Robert Dewar  <dewar@adacore.com>

	* exp_ch7.adb: Minor reformatting.
	* exp_unst.adb (Build_Tables): Fix minor glitch for no separate
	spec case.
	* erroutc.adb (Delete_Msg): add missing decrement of info msg counter.

2015-03-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb (Build_Pragma_Check_Equivalent): Suppress
	references to formal parameters subject to pragma Unreferenced.
	(Suppress_Reference): New routine.
	* sem_attr.adb (Analyze_Attribute): Reimplement the analysis
	of attribute 'Old. Attributes 'Old and 'Result now share
	common processing.
	(Analyze_Old_Result_Attribute): New routine.
	(Check_Placement_In_Check): Removed.
	(Check_Placement_In_Contract_Cases): Removed.
	(Check_Placement_In_Test_Case): Removed.
	(Check_Use_In_Contract_Cases): Removed.
	(Check_Use_In_Test_Case): Removed.
	(In_Refined_Post): Removed.
	(Is_Within): Removed.
	* sem_warn.adb (Check_Low_Bound_Tested): Code cleanup.
	(Check_Low_Bound_Tested_For): New routine.

2015-03-04  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch3.adb (Expand_N_Object_Declaration):
	Generate a runtime check to test the expression of pragma
	Default_Initial_Condition when the object is default initialized.

From-SVN: r221176

8 files changed, 509 insertions, 540 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6a7a17c..c48ea3f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,35 @@
+2015-03-04  Robert Dewar  <dewar@adacore.com>
+
+	* exp_ch7.adb: Minor reformatting.
+	* exp_unst.adb (Build_Tables): Fix minor glitch for no separate
+	spec case.
+	* erroutc.adb (Delete_Msg): add missing decrement of info msg counter.
+
+2015-03-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch6.adb (Build_Pragma_Check_Equivalent): Suppress
+	references to formal parameters subject to pragma Unreferenced.
+	(Suppress_Reference): New routine.
+	* sem_attr.adb (Analyze_Attribute): Reimplement the analysis
+	of attribute 'Old. Attributes 'Old and 'Result now share
+	common processing.
+	(Analyze_Old_Result_Attribute): New routine.
+	(Check_Placement_In_Check): Removed.
+	(Check_Placement_In_Contract_Cases): Removed.
+	(Check_Placement_In_Test_Case): Removed.
+	(Check_Use_In_Contract_Cases): Removed.
+	(Check_Use_In_Test_Case): Removed.
+	(In_Refined_Post): Removed.
+	(Is_Within): Removed.
+	* sem_warn.adb (Check_Low_Bound_Tested): Code cleanup.
+	(Check_Low_Bound_Tested_For): New routine.
+
+2015-03-04  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch3.adb (Expand_N_Object_Declaration):
+	Generate a runtime check to test the expression of pragma
+	Default_Initial_Condition when the object is default initialized.
+
 2015-03-02  Robert Dewar  <dewar@adacore.com>
 
 	* scng.adb (Scan): Ignore illegal character in relaxed
diff --git a/gcc/ada/erroutc.adb b/gcc/ada/erroutc.adb
index c76c1ce..041158a 100644
--- a/gcc/ada/erroutc.adb
+++ b/gcc/ada/erroutc.adb
@@ -141,6 +141,10 @@ package body Erroutc is
             if Errors.Table (D).Warn or else Errors.Table (D).Style then
                Warnings_Detected := Warnings_Detected - 1;
 
+               if Errors.Table (D).Info then
+                  Info_Messages := Info_Messages - 1;
+               end if;
+
                --  Note: we do not need to decrement Warnings_Treated_As_Errors
                --  because this only gets incremented if we actually output the
                --  message, which we won't do if we are deleting it here!
diff --git a/gcc/ada/exp_ch3.adb b/gcc/ada/exp_ch3.adb
index c2ba50a..0baa3f6 100644
--- a/gcc/ada/exp_ch3.adb
+++ b/gcc/ada/exp_ch3.adb
@@ -6138,11 +6138,9 @@ package body Exp_Ch3 is
          end;
       end if;
 
-      --  At this point the object is fully initialized by either invoking the
-      --  related type init proc, routine [Deep_]Initialize or performing in-
-      --  place assingments for an array object. If the related type is subject
-      --  to pragma Default_Initial_Condition, add a runtime check to verify
-      --  the assumption of the pragma. Generate:
+      --  If the object is default initialized and its type is subject to
+      --  pragma Default_Initial_Condition, add a runtime check to verify
+      --  the assumption of the pragma (SPARK RM 7.3.3). Generate:
 
       --    <Base_Typ>Default_Init_Cond (<Base_Typ> (Def_Id));
 
@@ -6152,6 +6150,7 @@ package body Exp_Ch3 is
         and then (Has_Default_Init_Cond           (Base_Typ)
                     or else
                   Has_Inherited_Default_Init_Cond (Base_Typ))
+        and then not Has_Init_Expression (N)
       then
          declare
             DIC_Call : constant Node_Id :=
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 4210968..ce3052e 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -7163,6 +7163,42 @@ package body Exp_Ch6 is
          Subp_Id  : Entity_Id := Empty;
          Inher_Id : Entity_Id := Empty) return Node_Id
       is
+         function Suppress_Reference (N : Node_Id) return Traverse_Result;
+         --  Detect whether node N references a formal parameter subject to
+         --  pragma Unreferenced. If this is the case, set Comes_From_Source
+         --  to False to suppress the generation of a reference when analyzing
+         --  N later on.
+
+         ------------------------
+         -- Suppress_Reference --
+         ------------------------
+
+         function Suppress_Reference (N : Node_Id) return Traverse_Result is
+            Formal : Entity_Id;
+
+         begin
+            if Is_Entity_Name (N) and then Present (Entity (N)) then
+               Formal := Entity (N);
+
+               --  The formal parameter is subject to pragma Unreferenced.
+               --  Prevent the generation of a reference by resetting the
+               --  Comes_From_Source flag.
+
+               if Is_Formal (Formal)
+                 and then Has_Pragma_Unreferenced (Formal)
+               then
+                  Set_Comes_From_Source (N, False);
+               end if;
+            end if;
+
+            return OK;
+         end Suppress_Reference;
+
+         procedure Suppress_References is
+           new Traverse_Proc (Suppress_Reference);
+
+         --  Local variables
+
          Loc          : constant Source_Ptr := Sloc (Prag);
          Prag_Nam     : constant Name_Id    := Pragma_Name (Prag);
          Check_Prag   : Node_Id;
@@ -7172,6 +7208,8 @@ package body Exp_Ch6 is
          Nam          : Name_Id;
          Subp_Formal  : Entity_Id;
 
+      --  Start of processing for Build_Pragma_Check_Equivalent
+
       begin
          Formals_Map := No_Elist;
 
@@ -7208,8 +7246,26 @@ package body Exp_Ch6 is
          --  Mark the pragma as being internally generated and reset the
          --  Analyzed flag.
 
-         Set_Comes_From_Source (Check_Prag, False);
          Set_Analyzed          (Check_Prag, False);
+         Set_Comes_From_Source (Check_Prag, False);
+
+         --  The tree of the original pragma may contain references to the
+         --  formal parameters of the related subprogram. At the same time
+         --  the corresponding body may mark the formals as unreferenced:
+
+         --     procedure Proc (Formal : ...)
+         --       with Pre => Formal ...;
+
+         --     procedure Proc (Formal : ...) is
+         --        pragma Unreferenced (Formal);
+         --     ...
+
+         --  This creates problems because all pragma Check equivalents are
+         --  analyzed at the end of the body declarations. Since all source
+         --  references have already been accounted for, reset any references
+         --  to such formals in the generated pragma Check equivalent.
+
+         Suppress_References (Check_Prag);
 
          if Present (Corresponding_Aspect (Prag)) then
             Nam := Chars (Identifier (Corresponding_Aspect (Prag)));
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 52dfb4e..2c6683d 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -7853,12 +7853,10 @@ package body Exp_Ch7 is
      (Loc     : Source_Ptr;
       Ptr_Typ : Entity_Id) return Node_Id
    is
-
-      --  It is possible for Ptr_Typ to be a partial view, if the access
-      --  type is a full view declared in the private part of a nested package,
-      --  and the finalization actions take place when completing analysis
-      --  of the enclosing unit. For this reason we use Underlying_Type
-      --  in two places below.
+      --  It is possible for Ptr_Typ to be a partial view, if the access type
+      --  is a full view declared in the private part of a nested package, and
+      --  the finalization actions take place when completing analysis of the
+      --  enclosing unit. For this reason use Underlying_Type twice below.
 
       Desig_Typ : constant Entity_Id :=
                     Available_View
diff --git a/gcc/ada/exp_unst.adb b/gcc/ada/exp_unst.adb
index 29746dc..2b143c5 100755
--- a/gcc/ada/exp_unst.adb
+++ b/gcc/ada/exp_unst.adb
@@ -491,16 +491,16 @@ package body Exp_Unst is
          --  then we won't catch it in the traversal of the body. But we do
          --  want to visit the declaration in this case!
 
-         declare
-            Dummy : Traverse_Result;
-            Decl  : constant Node_Id :=
-              Parent (Declaration_Node (Corresponding_Spec (Subp_Body)));
-            pragma Assert (Nkind (Decl) = N_Subprogram_Declaration);
-         begin
-            if not Acts_As_Spec (Subp_Body) then
+         if not Acts_As_Spec (Subp_Body) then
+            declare
+               Dummy : Traverse_Result;
+               Decl  : constant Node_Id :=
+                 Parent (Declaration_Node (Corresponding_Spec (Subp_Body)));
+               pragma Assert (Nkind (Decl) = N_Subprogram_Declaration);
+            begin
                Dummy := Visit_Node (Decl);
-            end if;
-         end;
+            end;
+         end if;
 
          --  Traverse the body to get the rest of the subprograms and calls
 
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index b3786f1..d4ece97 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -241,6 +241,15 @@ package body Sem_Attr is
       --  Used for Access, Unchecked_Access, Unrestricted_Access attributes.
       --  Internally, Id distinguishes which of the three cases is involved.
 
+      procedure Analyze_Attribute_Old_Result
+        (Legal   : out Boolean;
+         Spec_Id : out Entity_Id);
+      --  Common processing for attributes 'Old and 'Result. The routine checks
+      --  that the attribute appears in a postcondition-like aspect or pragma
+      --  associated with a suitable subprogram or a body. Flag Legal is set
+      --  when the above criterias are met. Spec_Id denotes the entity of the
+      --  subprogram [body] or Empty if the attribute is illegal.
+
       procedure Bad_Attribute_For_Predicate;
       --  Output error message for use of a predicate (First, Last, Range) not
       --  allowed with a type that has predicates. If the type is a generic
@@ -343,6 +352,9 @@ package body Sem_Attr is
       procedure Check_Object_Reference (P : Node_Id);
       --  Check that P is an object reference
 
+      procedure Check_PolyORB_Attribute;
+      --  Validity checking for PolyORB/DSA attribute
+
       procedure Check_Program_Unit;
       --  Verify that prefix of attribute N is a program unit
 
@@ -364,9 +376,6 @@ package body Sem_Attr is
       procedure Check_System_Prefix;
       --  Verify that prefix of attribute N is package System
 
-      procedure Check_PolyORB_Attribute;
-      --  Validity checking for PolyORB/DSA attribute
-
       procedure Check_Task_Prefix;
       --  Verify that prefix of attribute N is a task or task type
 
@@ -397,10 +406,6 @@ package body Sem_Attr is
       pragma No_Return (Error_Attr);
       --  Like Error_Attr, but error is posted at the start of the prefix
 
-      function In_Refined_Post return Boolean;
-      --  Determine whether the current attribute appears in pragma
-      --  Refined_Post.
-
       procedure Legal_Formal_Attribute;
       --  Common processing for attributes Definite and Has_Discriminants.
       --  Checks that prefix is generic indefinite formal type.
@@ -1072,6 +1077,263 @@ package body Sem_Attr is
          end if;
       end Analyze_Access_Attribute;
 
+      ----------------------------------
+      -- Analyze_Attribute_Old_Result --
+      ----------------------------------
+
+      procedure Analyze_Attribute_Old_Result
+        (Legal   : out Boolean;
+         Spec_Id : out Entity_Id)
+      is
+         procedure Check_Placement_In_Check (Prag : Node_Id);
+         --  Verify that the attribute appears within pragma Check that mimics
+         --  a postcondition.
+
+         procedure Check_Placement_In_Contract_Cases (Prag : Node_Id);
+         --  Verify that the attribute appears within a consequence of aspect
+         --  or pragma Contract_Cases denoted by Prag.
+
+         procedure Check_Placement_In_Test_Case (Prag : Node_Id);
+         --  Verify that the attribute appears within the "Ensures" argument of
+         --  aspect or pragma Test_Case denoted by Prag.
+
+         function Is_Within
+           (Nod      : Node_Id;
+            Encl_Nod : Node_Id) return Boolean;
+         --  Subsidiary to Check_Placemenet_In_XXX. Determine whether arbitrary
+         --  node Nod is within enclosing node Encl_Nod.
+
+         ------------------------------
+         -- Check_Placement_In_Check --
+         ------------------------------
+
+         procedure Check_Placement_In_Check (Prag : Node_Id) is
+            Args : constant List_Id := Pragma_Argument_Associations (Prag);
+            Nam  : constant Name_Id := Chars (Get_Pragma_Arg (First (Args)));
+
+         begin
+            --  The "Name" argument of pragma Check denotes a postcondition
+
+            if Nam_In (Nam, Name_Post,
+                            Name_Post_Class,
+                            Name_Postcondition,
+                            Name_Refined_Post)
+            then
+               null;
+
+            --  Otherwise the placement of the attribute is illegal
+
+            else
+               if Aname = Name_Old then
+                  Error_Attr
+                    ("attribute % can only appear in postcondition", P);
+
+               --  Specialize the error message for attribute 'Result
+
+               else
+                  Error_Attr
+                    ("attribute % can only appear in postcondition of "
+                     & "function", P);
+               end if;
+            end if;
+         end Check_Placement_In_Check;
+
+         ---------------------------------------
+         -- Check_Placement_In_Contract_Cases --
+         ---------------------------------------
+
+         procedure Check_Placement_In_Contract_Cases (Prag : Node_Id) is
+            Arg   : Node_Id;
+            Cases : Node_Id;
+            CCase : Node_Id;
+
+         begin
+            --  Obtain the argument of the aspect or pragma
+
+            if Nkind (Prag) = N_Aspect_Specification then
+               Arg := Prag;
+            else
+               Arg := First (Pragma_Argument_Associations (Prag));
+            end if;
+
+            Cases := Expression (Arg);
+
+            if Present (Component_Associations (Cases)) then
+               CCase := First (Component_Associations (Cases));
+               while Present (CCase) loop
+
+                  --  Detect whether the attribute appears within the
+                  --  consequence of the current contract case.
+
+                  if Nkind (CCase) = N_Component_Association
+                    and then Is_Within (N, Expression (CCase))
+                  then
+                     return;
+                  end if;
+
+                  Next (CCase);
+               end loop;
+            end if;
+
+            --  Otherwise aspect or pragma Contract_Cases is either malformed
+            --  or the attribute does not appear within a consequence.
+
+            Error_Attr
+              ("attribute % must appear in the consequence of a contract case",
+               P);
+         end Check_Placement_In_Contract_Cases;
+
+         ----------------------------------
+         -- Check_Placement_In_Test_Case --
+         ----------------------------------
+
+         procedure Check_Placement_In_Test_Case (Prag : Node_Id) is
+            Arg : constant Node_Id :=
+                    Test_Case_Arg
+                      (Prag        => Prag,
+                       Arg_Nam     => Name_Ensures,
+                       From_Aspect => Nkind (Prag) = N_Aspect_Specification);
+
+         begin
+            --  Detect whether the attribute appears within the "Ensures"
+            --  expression of aspect or pragma Test_Case.
+
+            if Present (Arg) and then Is_Within (N, Arg) then
+               null;
+
+            else
+               Error_Attr
+                 ("attribute % must appear in the ensures expression of a "
+                  & "test case", P);
+            end if;
+         end Check_Placement_In_Test_Case;
+
+         ---------------
+         -- Is_Within --
+         ---------------
+
+         function Is_Within
+           (Nod      : Node_Id;
+            Encl_Nod : Node_Id) return Boolean
+         is
+            Par : Node_Id;
+
+         begin
+            Par := Nod;
+            while Present (Par) loop
+               if Par = Encl_Nod then
+                  return True;
+
+               --  Prevent the search from going too far
+
+               elsif Is_Body_Or_Package_Declaration (Par) then
+                  exit;
+               end if;
+
+               Par := Parent (Par);
+            end loop;
+
+            return False;
+         end Is_Within;
+
+         --  Local variables
+
+         Prag      : Node_Id;
+         Prag_Nam  : Name_Id;
+         Subp_Decl : Node_Id;
+
+      --  Start of processing for Analyze_Attribute_Old_Result
+
+      begin
+         --  Assume that the attribute is illegal
+
+         Legal   := False;
+         Spec_Id := Empty;
+
+         --  Traverse the parent chain to find the aspect or pragma where the
+         --  attribute resides.
+
+         Prag := N;
+         while Present (Prag) loop
+            if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
+               exit;
+
+            --  Prevent the search from going too far
+
+            elsif Is_Body_Or_Package_Declaration (Prag) then
+               exit;
+            end if;
+
+            Prag := Parent (Prag);
+         end loop;
+
+         --  The attribute is allowed to appear only in postcondition-like
+         --  aspects or pragmas.
+
+         if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
+            if Nkind (Prag) = N_Aspect_Specification then
+               Prag_Nam := Chars (Identifier (Prag));
+            else
+               Prag_Nam := Pragma_Name (Prag);
+            end if;
+
+            if Prag_Nam = Name_Check then
+               Check_Placement_In_Check (Prag);
+
+            elsif Prag_Nam = Name_Contract_Cases then
+               Check_Placement_In_Contract_Cases (Prag);
+
+            elsif Nam_In (Prag_Nam, Name_Post,
+                                    Name_Post_Class,
+                                    Name_Postcondition,
+                                    Name_Refined_Post)
+            then
+               null;
+
+            elsif Prag_Nam = Name_Test_Case then
+               Check_Placement_In_Test_Case (Prag);
+
+            else
+               Error_Attr ("attribute % can only appear in postcondition", P);
+               return;
+            end if;
+
+         --  Otherwise the placement of the attribute is illegal
+
+         else
+            Error_Attr ("attribute % can only appear in postcondition", P);
+            return;
+         end if;
+
+         --  Find the related subprogram subject to the aspect or pragma
+
+         if Nkind (Prag) = N_Aspect_Specification then
+            Subp_Decl := Parent (Prag);
+         else
+            Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
+         end if;
+
+         --  The aspect or pragma where the attribute resides should be
+         --  associated with a subprogram declaration or a body. If this is not
+         --  the case, then the aspect or pragma is illegal. Return as analysis
+         --  cannot be carried out.
+
+         if not Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
+                                     N_Entry_Declaration,
+                                     N_Generic_Subprogram_Declaration,
+                                     N_Subprogram_Body,
+                                     N_Subprogram_Body_Stub,
+                                     N_Subprogram_Declaration)
+         then
+            return;
+         end if;
+
+         --  If we get here, then the attribute is legal
+
+         Legal   := True;
+         Spec_Id := Corresponding_Spec_Of (Subp_Decl);
+      end Analyze_Attribute_Old_Result;
+
       ---------------------------------
       -- Bad_Attribute_For_Predicate --
       ---------------------------------
@@ -2175,60 +2437,6 @@ package body Sem_Attr is
          Error_Attr;
       end Error_Attr_P;
 
-      ---------------------
-      -- In_Refined_Post --
-      ---------------------
-
-      function In_Refined_Post return Boolean is
-         function Is_Refined_Post (Prag : Node_Id) return Boolean;
-         --  Determine whether Prag denotes one of the incarnations of pragma
-         --  Refined_Post (either as is or pragma Check (Refined_Post, ...).
-
-         ---------------------
-         -- Is_Refined_Post --
-         ---------------------
-
-         function Is_Refined_Post (Prag : Node_Id) return Boolean is
-            Args : constant List_Id := Pragma_Argument_Associations (Prag);
-            Nam  : constant Name_Id := Pragma_Name (Prag);
-
-         begin
-            if Nam = Name_Refined_Post then
-               return True;
-
-            elsif Nam = Name_Check then
-               pragma Assert (Present (Args));
-
-               return Chars (Expression (First (Args))) = Name_Refined_Post;
-            end if;
-
-            return False;
-         end Is_Refined_Post;
-
-         --  Local variables
-
-         Stmt : Node_Id;
-
-      --  Start of processing for In_Refined_Post
-
-      begin
-         Stmt := Parent (N);
-         while Present (Stmt) loop
-            if Nkind (Stmt) = N_Pragma and then Is_Refined_Post (Stmt) then
-               return True;
-
-            --  Prevent the search from going too far
-
-            elsif Is_Body_Or_Package_Declaration (Stmt) then
-               exit;
-            end if;
-
-            Stmt := Parent (Stmt);
-         end loop;
-
-         return False;
-      end In_Refined_Post;
-
       ----------------------------
       -- Legal_Formal_Attribute --
       ----------------------------
@@ -4462,14 +4670,6 @@ package body Sem_Attr is
          --  the related postcondition expression. Subp_Id is the subprogram to
          --  which the related postcondition applies.
 
-         procedure Check_Use_In_Contract_Cases (Prag : Node_Id);
-         --  Perform various semantic checks related to the placement of the
-         --  attribute in pragma Contract_Cases.
-
-         procedure Check_Use_In_Test_Case (Prag : Node_Id);
-         --  Perform various semantic checks related to the placement of the
-         --  attribute in pragma Contract_Cases.
-
          --------------------------------
          -- Check_References_In_Prefix --
          --------------------------------
@@ -4504,7 +4704,7 @@ package body Sem_Attr is
                --  case, then the scope of the local entity is nested within
                --  that of the subprogram.
 
-               elsif Nkind (Nod) = N_Identifier
+               elsif Is_Entity_Name (Nod)
                  and then Present (Entity (Nod))
                  and then Scope_Within (Scope (Entity (Nod)), Subp_Id)
                then
@@ -4512,6 +4712,9 @@ package body Sem_Attr is
                     ("prefix of attribute % cannot reference local entities",
                      Nod);
                   return Abandon;
+
+               --  Otherwise keep inspecting the prefix
+
                else
                   return OK;
                end if;
@@ -4525,261 +4728,130 @@ package body Sem_Attr is
             Check_References (P);
          end Check_References_In_Prefix;
 
-         ---------------------------------
-         -- Check_Use_In_Contract_Cases --
-         ---------------------------------
-
-         procedure Check_Use_In_Contract_Cases (Prag : Node_Id) is
-            Cases : constant Node_Id :=
-                      Get_Pragma_Arg
-                        (First (Pragma_Argument_Associations (Prag)));
-            Expr  : Node_Id;
-
-         begin
-            --  Climb the parent chain to reach the top of the expression where
-            --  attribute 'Old resides.
-
-            Expr := N;
-            while Parent (Parent (Expr)) /= Cases loop
-               Expr := Parent (Expr);
-            end loop;
-
-            --  Ensure that the obtained expression is the consequence of a
-            --  contract case as this is the only postcondition-like part of
-            --  the pragma. Otherwise, attribute 'Old appears in the condition
-            --  of a contract case. Emit an error since this is not a
-            --  postcondition-like context. (SPARK RM 6.1.3(2))
-
-            if Expr /= Expression (Parent (Expr)) then
-               Error_Attr
-                 ("attribute % cannot appear in the condition "
-                  & "of a contract case", P);
-            end if;
-         end Check_Use_In_Contract_Cases;
-
-         ----------------------------
-         -- Check_Use_In_Test_Case --
-         ----------------------------
-
-         procedure Check_Use_In_Test_Case (Prag : Node_Id) is
-            Ensures : constant Node_Id := Test_Case_Arg (Prag, Name_Ensures);
-            Expr    : Node_Id;
-
-         begin
-            --  Climb the parent chain to reach the top of the Ensures part of
-            --  pragma Test_Case.
-
-            Expr := N;
-            while Expr /= Prag loop
-               if Expr = Ensures then
-                  return;
-               end if;
-
-               Expr := Parent (Expr);
-            end loop;
-
-            --  If we get there, then attribute 'Old appears in the requires
-            --  expression of pragma Test_Case which is not a postcondition-
-            --  like context.
-
-            Error_Attr
-              ("attribute % cannot appear in the requires expression of a "
-               & "test case", P);
-         end Check_Use_In_Test_Case;
-
          --  Local variables
 
-         CS : Entity_Id;
-         --  The enclosing scope, excluding loops for quantified expressions.
-         --  During analysis, it is the postcondition subprogram. During
-         --  pre-analysis, it is the scope of the subprogram declaration.
-
-         Prag : Node_Id;
-         --  During pre-analysis, Prag is the enclosing pragma node if any
+         Legal    : Boolean;
+         Pref_Id  : Entity_Id;
+         Pref_Typ : Entity_Id;
+         Spec_Id  : Entity_Id;
 
       --  Start of processing for Old
 
       begin
-         Prag := Empty;
-
-         --  Find enclosing scopes, excluding loops
-
-         CS := Current_Scope;
-         while Ekind (CS) = E_Loop loop
-            CS := Scope (CS);
-         end loop;
-
-         --  Check the legality of attribute 'Old when it appears inside pragma
-         --  Refined_Post. These specialized checks are required only when code
-         --  generation is disabled. In the general case pragma Refined_Post is
-         --  transformed into pragma Check by Process_PPCs which in turn is
-         --  relocated to procedure _Postconditions. From then on the legality
-         --  of 'Old is determined as usual.
+         --  The attribute reference is a primary. If any expressions follow,
+         --  then the attribute reference is an indexable object. Transform the
+         --  attribute into an indexed component and analyze it.
 
-         if not Expander_Active and then In_Refined_Post then
-            Preanalyze_And_Resolve (P);
-            Check_References_In_Prefix (CS);
-            P_Type := Etype (P);
-            Set_Etype (N, P_Type);
+         if Present (E1) then
+            Rewrite (N,
+              Make_Indexed_Component (Loc,
+                Prefix      =>
+                  Make_Attribute_Reference (Loc,
+                    Prefix         => Relocate_Node (P),
+                    Attribute_Name => Name_Old),
+                Expressions => Expressions (N)));
+            Analyze (N);
+            return;
+         end if;
 
-            if Is_Limited_Type (P_Type) then
-               Error_Attr ("attribute % cannot apply to limited objects", P);
-            end if;
+         Analyze_Attribute_Old_Result (Legal, Spec_Id);
 
-            if Is_Entity_Name (P)
-              and then Is_Constant_Object (Entity (P))
-            then
-               Error_Msg_N
-                 ("??attribute Old applied to constant has no effect", P);
-            end if;
+         --  The aspect or pragma where attribute 'Old resides should be
+         --  associated with a subprogram declaration or a body. If this is not
+         --  the case, then the aspect or pragma is illegal. Return as analysis
+         --  cannot be carried out.
 
+         if not Legal then
             return;
+         end if;
 
-         --  A Contract_Cases, Postcondition or Test_Case pragma is in the
-         --  process of being preanalyzed. Perform the semantic checks now
-         --  before the pragma is relocated and/or expanded.
-
-         --  For a generic subprogram, postconditions are preanalyzed as well
-         --  for name capture, and still appear within an aspect spec.
-
-         elsif In_Spec_Expression or Inside_A_Generic then
-            Prag := N;
-            while Present (Prag)
-               and then not Nkind_In (Prag, N_Aspect_Specification,
-                                            N_Function_Specification,
-                                            N_Pragma,
-                                            N_Procedure_Specification,
-                                            N_Subprogram_Body)
-            loop
-               Prag := Parent (Prag);
-            end loop;
-
-            --  In ASIS mode, the aspect itself is analyzed, in addition to the
-            --  corresponding pragma. Don't issue errors when analyzing aspect.
+         --  The prefix must be preanalyzed as the full analysis will take
+         --  place during expansion.
 
-            if Nkind (Prag) = N_Aspect_Specification
-              and then Nam_In (Chars (Identifier (Prag)), Name_Post,
-                                                          Name_Refined_Post)
-            then
-               null;
+         Preanalyze_And_Resolve (P);
 
-            --  In all other cases the related context must be a pragma
+         --  Ensure that the prefix does not contain attributes 'Old or 'Result
 
-            elsif Nkind (Prag) /= N_Pragma then
-               Error_Attr ("% attribute can only appear in postcondition", P);
+         Check_References_In_Prefix (Spec_Id);
 
-            --  Verify the placement of the attribute with respect to the
-            --  related pragma.
+         --  Set the type of the attribute now to prevent cascaded errors
 
-            else
-               case Get_Pragma_Id (Prag) is
-                  when Pragma_Contract_Cases =>
-                     Check_Use_In_Contract_Cases (Prag);
+         Pref_Typ := Etype (P);
+         Set_Etype (N, Pref_Typ);
 
-                  when Pragma_Postcondition | Pragma_Refined_Post =>
-                     null;
+         --  Legality checks
 
-                  when Pragma_Test_Case =>
-                     Check_Use_In_Test_Case (Prag);
+         if Is_Limited_Type (Pref_Typ) then
+            Error_Attr ("attribute % cannot apply to limited objects", P);
+         end if;
 
-                  when others =>
-                     Error_Attr
-                       ("% attribute can only appear in postcondition", P);
-               end case;
-            end if;
+         --  The prefix is a simple name
 
-         --  Body case, where we must be inside a generated _Postconditions
-         --  procedure, or else the attribute use is definitely misplaced. The
-         --  postcondition itself may have generated transient scopes, and is
-         --  not necessarily the current one.
+         if Is_Entity_Name (P) and then Present (Entity (P)) then
+            Pref_Id := Entity (P);
 
-         else
-            while Present (CS) and then CS /= Standard_Standard loop
-               if Chars (CS) = Name_uPostconditions then
-                  exit;
-               else
-                  CS := Scope (CS);
-               end if;
-            end loop;
+            --  Emit a warning when the prefix is a constant. Note that the use
+            --  of Error_Attr would reset the type of N to Any_Type even though
+            --  this is a warning. Use Error_Msg_XXX instead.
 
-            if Chars (CS) /= Name_uPostconditions then
-               Error_Attr ("% attribute can only appear in postcondition", P);
+            if Is_Constant_Object (Pref_Id) then
+               Error_Msg_Name_1 := Name_Old;
+               Error_Msg_N
+                 ("??atribute % applied to constant has no effect", P);
             end if;
-         end if;
 
-         --  If the attribute reference is generated for a Requires clause,
-         --  then no expressions follow. Otherwise it is a primary, in which
-         --  case, if expressions follow, the attribute reference must be an
-         --  indexable object, so rewrite the node accordingly.
+         --  Otherwise the prefix is not a simple name
 
-         if Present (E1) then
-            Rewrite (N,
-              Make_Indexed_Component (Loc,
-                Prefix      =>
-                  Make_Attribute_Reference (Loc,
-                    Prefix         => Relocate_Node (Prefix (N)),
-                    Attribute_Name => Name_Old),
-                Expressions => Expressions (N)));
+         else
+            --  Ensure that the prefix of attribute 'Old is an entity when it
+            --  is potentially unevaluated (6.1.1 (27/3)).
 
-            Analyze (N);
-            return;
-         end if;
+            if Is_Potentially_Unevaluated (N) then
+               Uneval_Old_Msg;
 
-         Check_E0;
+            --  Detect a possible infinite recursion when the prefix denotes
+            --  the related function.
 
-         --  Prefix has not been analyzed yet, and its full analysis will take
-         --  place during expansion (see below).
+            --    function Func (...) return ...
+            --      with Post => Func'Old ...;
 
-         Preanalyze_And_Resolve (P);
-         Check_References_In_Prefix (CS);
-         P_Type := Etype (P);
-         Set_Etype (N, P_Type);
+            elsif Nkind (P) = N_Function_Call then
+               Pref_Id := Entity (Name (P));
 
-         if Is_Limited_Type (P_Type) then
-            Error_Attr ("attribute % cannot apply to limited objects", P);
-         end if;
+               if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+                 and then Pref_Id = Spec_Id
+               then
+                  Error_Msg_Warn := SPARK_Mode /= On;
+                  Error_Msg_N ("!possible infinite recursion<<", P);
+                  Error_Msg_N ("\!??Storage_Error ]<<", P);
+               end if;
+            end if;
 
-         if Is_Entity_Name (P)
-           and then Is_Constant_Object (Entity (P))
-         then
-            Error_Msg_N
-              ("??attribute Old applied to constant has no effect", P);
-         end if;
+            --  The prefix of attribute 'Old may refer to a component of a
+            --  formal parameter. In this case its expansion may generate
+            --  actual subtypes that are referenced in an inner context and
+            --  that must be elaborated within the subprogram itself. If the
+            --  prefix includes a function call, it may involve finalization
+            --  actions that should be inserted when the attribute has been
+            --  rewritten as a declaration. Create a declaration for the prefix
+            --  and insert it at the start of the enclosing subprogram. This is
+            --  an expansion activity that has to be performed now to prevent
+            --  out-of-order issues.
 
-         --  Check that the prefix of 'Old is an entity when it may be
-         --  potentially unevaluated (6.1.1 (27/3)).
+            --  This expansion is both harmful and not needed in SPARK mode,
+            --  since the formal verification backend relies on the types of
+            --  nodes (hence is not robust w.r.t. a change to base type here),
+            --  and does not suffer from the out-of-order issue described
+            --  above. Thus, this expansion is skipped in SPARK mode.
 
-         if Present (Prag)
-           and then Is_Potentially_Unevaluated (N)
-           and then not Is_Entity_Name (P)
-         then
-            Uneval_Old_Msg;
-         end if;
+            if not GNATprove_Mode then
+               Pref_Typ := Base_Type (Pref_Typ);
+               Set_Etype (N, Pref_Typ);
+               Set_Etype (P, Pref_Typ);
 
-         --  The attribute appears within a pre/postcondition, but refers to
-         --  an entity in the enclosing subprogram. If it is a component of
-         --  a formal its expansion might generate actual subtypes that may
-         --  be referenced in an inner context, and which must be elaborated
-         --  within the subprogram itself. If the prefix includes a function
-         --  call it may involve finalization actions that should only be
-         --  inserted when the attribute has been rewritten as a declarations.
-         --  As a result, if the prefix is not a simple name we create
-         --  a declaration for it now, and insert it at the start of the
-         --  enclosing subprogram. This is properly an expansion activity
-         --  but it has to be performed now to prevent out-of-order issues.
-
-         --  This expansion is both harmful and not needed in SPARK mode, since
-         --  the formal verification backend relies on the types of nodes
-         --  (hence is not robust w.r.t. a change to base type here), and does
-         --  not suffer from the out-of-order issue described above. Thus, this
-         --  expansion is skipped in SPARK mode.
-
-         if not Is_Entity_Name (P) and then not GNATprove_Mode then
-            P_Type := Base_Type (P_Type);
-            Set_Etype (N, P_Type);
-            Set_Etype (P, P_Type);
-            Analyze_Dimension (N);
-            Expand (N);
+               Analyze_Dimension (N);
+               Expand (N);
+            end if;
          end if;
       end Old;
 
@@ -4985,105 +5057,12 @@ package body Sem_Attr is
       ------------
 
       when Attribute_Result => Result : declare
-         procedure Check_Placement_In_Check (Prag : Node_Id);
-         --  Verify that attribute 'Result appears within pragma Check that
-         --  emulates a postcondition.
-
-         procedure Check_Placement_In_Contract_Cases (Prag : Node_Id);
-         --  Verify that attribute 'Result appears within a consequence of
-         --  pragma Contract_Cases.
-
-         procedure Check_Placement_In_Test_Case (Prag : Node_Id);
-         --  Verify that attribute 'Result appears within the Ensures argument
-         --  of pragma Test_Case.
-
          function Denote_Same_Function
            (Pref_Id : Entity_Id;
             Spec_Id : Entity_Id) return Boolean;
          --  Determine whether the entity of the prefix Pref_Id denotes the
          --  same entity as that of the related subprogram Spec_Id.
 
-         function Is_Within
-           (Nod      : Node_Id;
-            Encl_Nod : Node_Id) return Boolean;
-         --  Subsidiary to Check_Placemenet_In_XXX_Case. Determine whether
-         --  arbitrary node Nod is within enclosing node Encl_Nod.
-
-         ------------------------------
-         -- Check_Placement_In_Check --
-         ------------------------------
-
-         procedure Check_Placement_In_Check (Prag : Node_Id) is
-            Args : constant List_Id := Pragma_Argument_Associations (Prag);
-            Nam  : constant Name_Id := Chars (Get_Pragma_Arg (First (Args)));
-
-         begin
-            --  The "Name" argument of pragma Check denotes a postcondition
-
-            if Nam_In (Nam, Name_Post,
-                            Name_Postcondition,
-                            Name_Refined_Post)
-            then
-               null;
-
-            --  Otherwise the placement of attribute 'Result is illegal
-
-            else
-               Error_Attr
-                 ("% attribute can only appear in postcondition of function",
-                  P);
-            end if;
-         end Check_Placement_In_Check;
-
-         ---------------------------------------
-         -- Check_Placement_In_Contract_Cases --
-         ---------------------------------------
-
-         procedure Check_Placement_In_Contract_Cases (Prag : Node_Id) is
-            Args  : constant List_Id := Pragma_Argument_Associations (Prag);
-            Cases : constant Node_Id := Get_Pragma_Arg (First (Args));
-            CCase : Node_Id;
-
-         begin
-            if Present (Component_Associations (Cases)) then
-               CCase := First (Component_Associations (Cases));
-               while Present (CCase) loop
-
-                  --  Guard against a malformed contract case. Detect whether
-                  --  attribute 'Result appears within the consequence of the
-                  --  current contract case.
-
-                  if Nkind (CCase) = N_Component_Association
-                    and then Is_Within (N, Expression (CCase))
-                  then
-                     return;
-                  end if;
-
-                  Next (CCase);
-               end loop;
-            end if;
-
-            --  Otherwise pragma Contract_Cases is either malformed in some
-            --  way or attribute 'Result does not appear within a consequence
-            --  expression.
-
-            Error_Attr ("% attribute misplaced inside contract cases", P);
-         end Check_Placement_In_Contract_Cases;
-
-         ----------------------------------
-         -- Check_Placement_In_Test_Case --
-         ----------------------------------
-
-         procedure Check_Placement_In_Test_Case (Prag : Node_Id) is
-         begin
-            --  Detect whether attribute 'Result appears within the "Ensures"
-            --  expression of pragma Test_Case.
-
-            if not Is_Within (N, Test_Case_Arg (Prag, Name_Ensures)) then
-               Error_Attr ("% attribute misplaced inside test case", P);
-            end if;
-         end Check_Placement_In_Test_Case;
-
          --------------------------
          -- Denote_Same_Function --
          --------------------------
@@ -5135,41 +5114,11 @@ package body Sem_Attr is
             end if;
          end Denote_Same_Function;
 
-         ---------------
-         -- Is_Within --
-         ---------------
-
-         function Is_Within
-           (Nod      : Node_Id;
-            Encl_Nod : Node_Id) return Boolean
-         is
-            Par : Node_Id;
-
-         begin
-            Par := Nod;
-            while Present (Par) loop
-               if Par = Encl_Nod then
-                  return True;
-
-               --  Prevent the search from going too far
-
-               elsif Is_Body_Or_Package_Declaration (Par) then
-                  exit;
-               end if;
-
-               Par := Parent (Par);
-            end loop;
-
-            return False;
-         end Is_Within;
-
          --  Local variables
 
-         Prag      : Node_Id;
-         Prag_Id   : Pragma_Id;
-         Pref_Id   : Entity_Id;
-         Spec_Id   : Entity_Id;
-         Subp_Decl : Node_Id;
+         Legal   : Boolean;
+         Pref_Id : Entity_Id;
+         Spec_Id : Entity_Id;
 
       --  Start of processing for Result
 
@@ -5190,91 +5139,17 @@ package body Sem_Attr is
             return;
          end if;
 
-         --  Traverse the parent chain to find the aspect or pragma where
-         --  attribute 'Result resides.
-
-         Prag := N;
-         while Present (Prag) loop
-            if Nkind_In (Prag, N_Aspect_Specification, N_Pragma) then
-               exit;
-
-            --  Prevent the search from going too far
-
-            elsif Is_Body_Or_Package_Declaration (Prag) then
-               exit;
-            end if;
-
-            Prag := Parent (Prag);
-         end loop;
-
-         --  Do not emit an error when preanalyzing an aspect for ASIS. If the
-         --  placement of attribute 'Result is illegal, the error is reported
-         --  when analyzing the corresponding pragma.
-
-         if ASIS_Mode and then Nkind (Prag) = N_Aspect_Specification then
-            null;
-
-         --  Attribute 'Result is allowed to appear only in postcondition-like
-         --  pragmas.
-
-         elsif Nkind (Prag) = N_Pragma then
-            Prag_Id := Get_Pragma_Id (Prag);
-
-            if Prag_Id = Pragma_Check then
-               Check_Placement_In_Check (Prag);
-
-            elsif Prag_Id = Pragma_Contract_Cases then
-               Check_Placement_In_Contract_Cases (Prag);
-
-            elsif Prag_Id = Pragma_Postcondition
-              or else Prag_Id = Pragma_Refined_Post
-            then
-               null;
-
-            elsif Prag_Id = Pragma_Test_Case then
-               Check_Placement_In_Test_Case (Prag);
-
-            else
-               Error_Attr
-                 ("% attribute can only appear in postcondition of function",
-                  P);
-               return;
-            end if;
-
-         --  Otherwise the placement of the attribute is illegal
-
-         else
-            Error_Attr
-              ("% attribute can only appear in postcondition of function", P);
-            return;
-         end if;
-
-         --  Attribute 'Result appears within a postcondition-like pragma. Find
-         --  the related subprogram subject to the pragma.
+         Analyze_Attribute_Old_Result (Legal, Spec_Id);
 
-         if Nkind (Prag) = N_Aspect_Specification then
-            Subp_Decl := Parent (Prag);
-         else
-            Subp_Decl := Find_Related_Subprogram_Or_Body (Prag);
-         end if;
-
-         --  The pragma where attribute 'Result resides should be associated
-         --  with a subprogram declaration or a body. If this is not the case,
-         --  then the pragma is illegal. Return as analysis cannot be carried
-         --  out.
+         --  The aspect or pragma where attribute 'Result resides should be
+         --  associated with a subprogram declaration or a body. If this is not
+         --  the case, then the aspect or pragma is illegal. Return as analysis
+         --  cannot be carried out.
 
-         if not Nkind_In (Subp_Decl, N_Abstract_Subprogram_Declaration,
-                                     N_Entry_Declaration,
-                                     N_Generic_Subprogram_Declaration,
-                                     N_Subprogram_Body,
-                                     N_Subprogram_Body_Stub,
-                                     N_Subprogram_Declaration)
-         then
+         if not Legal then
             return;
          end if;
 
-         Spec_Id := Corresponding_Spec_Of (Subp_Decl);
-
          --  Attribute 'Result is part of a _Postconditions procedure. There is
          --  no need to perform the semantic checks below as they were already
          --  verified when the attribute was analyzed in its original context.
@@ -5309,7 +5184,7 @@ package body Sem_Attr is
                   else
                      Error_Msg_Name_2 := Chars (Spec_Id);
                      Error_Attr
-                       ("incorrect prefix for % attribute, expected %", P);
+                       ("incorrect prefix for attribute %, expected %", P);
                   end if;
 
                --  Otherwise the prefix denotes some other form of subprogram
@@ -5317,7 +5192,7 @@ package body Sem_Attr is
 
                else
                   Error_Attr
-                    ("% attribute can only appear in postcondition of "
+                    ("attribute % can only appear in postcondition of "
                      & "function", P);
                end if;
 
@@ -5325,7 +5200,7 @@ package body Sem_Attr is
 
             else
                Error_Msg_Name_2 := Chars (Spec_Id);
-               Error_Attr ("incorrect prefix for % attribute, expected %", P);
+               Error_Attr ("incorrect prefix for attribute %, expected %", P);
             end if;
          end if;
       end Result;
diff --git a/gcc/ada/sem_warn.adb b/gcc/ada/sem_warn.adb
index 7e1442f..b0e8011 100644
--- a/gcc/ada/sem_warn.adb
+++ b/gcc/ada/sem_warn.adb
@@ -723,28 +723,33 @@ package body Sem_Warn is
    ----------------------------
 
    procedure Check_Low_Bound_Tested (Expr : Node_Id) is
+      procedure Check_Low_Bound_Tested_For (Opnd : Node_Id);
+      --  Determine whether operand Opnd denotes attribute 'First whose prefix
+      --  is a formal parameter. If this is the case, mark the entity of the
+      --  prefix as having its low bound tested.
+
+      --------------------------------
+      -- Check_Low_Bound_Tested_For --
+      --------------------------------
+
+      procedure Check_Low_Bound_Tested_For (Opnd : Node_Id) is
+      begin
+         if Nkind (Opnd) = N_Attribute_Reference
+           and then Attribute_Name (Opnd) = Name_First
+           and then Is_Entity_Name (Prefix (Opnd))
+           and then Present (Entity (Prefix (Opnd)))
+           and then Is_Formal (Entity (Prefix (Opnd)))
+         then
+            Set_Low_Bound_Tested (Entity (Prefix (Opnd)));
+         end if;
+      end Check_Low_Bound_Tested_For;
+
+   --  Start of processing for Check_Low_Bound_Tested
+
    begin
       if Comes_From_Source (Expr) then
-         declare
-            L : constant Node_Id := Left_Opnd (Expr);
-            R : constant Node_Id := Right_Opnd (Expr);
-         begin
-            if Nkind (L) = N_Attribute_Reference
-              and then Attribute_Name (L) = Name_First
-              and then Is_Entity_Name (Prefix (L))
-              and then Is_Formal (Entity (Prefix (L)))
-            then
-               Set_Low_Bound_Tested (Entity (Prefix (L)));
-            end if;
-
-            if Nkind (R) = N_Attribute_Reference
-              and then Attribute_Name (R) = Name_First
-              and then Is_Entity_Name (Prefix (R))
-              and then Is_Formal (Entity (Prefix (R)))
-            then
-               Set_Low_Bound_Tested (Entity (Prefix (R)));
-            end if;
-         end;
+         Check_Low_Bound_Tested_For (Left_Opnd  (Expr));
+         Check_Low_Bound_Tested_For (Right_Opnd (Expr));
       end if;
    end Check_Low_Bound_Tested;