exp_ch6.adb: Remove with and use clause for Sem_Prag.

2013-04-24  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch6.adb: Remove with and use clause for Sem_Prag.
	(Freeze_Subprogram): Call Analyze_Subprogram_Contract to analyze
	the contract of a subprogram.
	* sem_ch3.adb: Remove with and use clause for Sem_Prag.
	(Analyze_Declarations): Call Analyze_Subprogram_Contract to
	analyze the contract of a subprogram.
	* sem_ch6.adb (Analyze_Subprogram_Contract): New routine.
	(Check_Subprogram_Contract): Removed.
	* sem_ch6.ads (Analyze_Subprogram_Contract): New routine.
	(Check_Subprogram_Contract): Removed.
	(Expand_Contract_Cases): Add a guard against malformed contract cases.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Call
	Decorate_Delayed_Aspect_And_Pragma to decorate aspects
	Contract_Cases, Depends and Global. Reimplement the analysis of
	aspect Contract_Cases.
	(Decorate_Delayed_Aspect_And_Pragma): New routine.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): New routine.
	(Analyze_CTC_In_Decl_Part): Removed.
	(Analyze_Pragma): Reimplement the analysis of pragma Contract_Cases.
	(Analyze_Test_Case_In_Decl_Part): New routine.
	(Find_Related_Subprogram): New routine.
	(Requires_Profile_Installation): Add new formal Prag. Update
	the logic to take into account the origin of the pragma.
	* sem_prag.ads (Analyze_Contract_Cases_In_Decl_Part): New routine.
	(Analyze_CTC_In_Decl_Part): Removed.
	(Analyze_Test_Case_In_Decl_Part): New routine.

From-SVN: r198227

8 files changed, 610 insertions, 758 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 92076bad0f8..93955a03843 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,32 @@
+2013-04-24  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch6.adb: Remove with and use clause for Sem_Prag.
+	(Freeze_Subprogram): Call Analyze_Subprogram_Contract to analyze
+	the contract of a subprogram.
+	* sem_ch3.adb: Remove with and use clause for Sem_Prag.
+	(Analyze_Declarations): Call Analyze_Subprogram_Contract to
+	analyze the contract of a subprogram.
+	* sem_ch6.adb (Analyze_Subprogram_Contract): New routine.
+	(Check_Subprogram_Contract): Removed.
+	* sem_ch6.ads (Analyze_Subprogram_Contract): New routine.
+	(Check_Subprogram_Contract): Removed.
+	(Expand_Contract_Cases): Add a guard against malformed contract cases.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Call
+	Decorate_Delayed_Aspect_And_Pragma to decorate aspects
+	Contract_Cases, Depends and Global. Reimplement the analysis of
+	aspect Contract_Cases.
+	(Decorate_Delayed_Aspect_And_Pragma): New routine.
+	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part): New routine.
+	(Analyze_CTC_In_Decl_Part): Removed.
+	(Analyze_Pragma): Reimplement the analysis of pragma Contract_Cases.
+	(Analyze_Test_Case_In_Decl_Part): New routine.
+	(Find_Related_Subprogram): New routine.
+	(Requires_Profile_Installation): Add new formal Prag. Update
+	the logic to take into account the origin of the pragma.
+	* sem_prag.ads (Analyze_Contract_Cases_In_Decl_Part): New routine.
+	(Analyze_CTC_In_Decl_Part): Removed.
+	(Analyze_Test_Case_In_Decl_Part): New routine.
+
 2013-04-24  Robert Dewar  <dewar@adacore.com>
 
 	* sem_prag.adb (Process_Convention): Move Stdcall tests to
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index c06a22434dc..bd6bb705bc8 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -67,7 +67,6 @@ with Sem_Disp; use Sem_Disp;
 with Sem_Dist; use Sem_Dist;
 with Sem_Eval; use Sem_Eval;
 with Sem_Mech; use Sem_Mech;
-with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_SCIL; use Sem_SCIL;
 with Sem_Util; use Sem_Util;
@@ -8304,31 +8303,7 @@ package body Exp_Ch6 is
       if Nkind (Parent (Subp)) = N_Procedure_Specification
         and then Null_Present (Parent (Subp))
       then
-         declare
-            Prag : Node_Id;
-
-         begin
-            --  Analyze all pre- and post-conditions
-
-            Prag := Pre_Post_Conditions (Contract (Subp));
-            while Present (Prag) loop
-               Analyze_PPC_In_Decl_Part (Prag, Subp);
-               Prag := Next_Pragma (Prag);
-            end loop;
-
-            --  Analyze classification aspects Depends and Global
-
-            Prag := Classifications (Contract (Subp));
-            while Present (Prag) loop
-               if Pragma_Name (Prag) = Name_Depends then
-                  Analyze_Depends_In_Decl_Part (Prag);
-               else
-                  Analyze_Global_In_Decl_Part (Prag);
-               end if;
-
-               Prag := Next_Pragma (Prag);
-            end loop;
-         end;
+         Analyze_Subprogram_Contract (Subp);
       end if;
    end Freeze_Subprogram;
 
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 31f5ab82602..30aa61eaf9c 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -925,11 +925,33 @@ package body Sem_Ch13 is
    -----------------------------------
 
    procedure Analyze_Aspect_Specifications (N : Node_Id; E : Entity_Id) is
+      procedure Decorate_Delayed_Aspect_And_Pragma
+        (Asp  : Node_Id;
+         Prag : Node_Id);
+      --  Establish the linkages between a delayed aspect and its corresponding
+      --  pragma. Set all delay-related flags on both constructs.
+
       procedure Insert_Delayed_Pragma (Prag : Node_Id);
       --  Insert a postcondition-like pragma into the tree depending on the
-      --  context. Prag one of the following: Pre, Post, Depends or Global.
+      --  context. Prag must denote one of the following: Pre, Post, Depends,
+      --  Global or Contract_Cases.
+
+      ----------------------------------------
+      -- Decorate_Delayed_Aspect_And_Pragma --
+      ----------------------------------------
 
-      --  Why not also Contract_Cases ???
+      procedure Decorate_Delayed_Aspect_And_Pragma
+        (Asp  : Node_Id;
+         Prag : Node_Id)
+      is
+      begin
+         Set_Aspect_Rep_Item           (Asp, Prag);
+         Set_Corresponding_Aspect      (Prag, Asp);
+         Set_From_Aspect_Specification (Prag);
+         Set_Is_Delayed_Aspect         (Prag);
+         Set_Is_Delayed_Aspect         (Asp);
+         Set_Parent                    (Prag, Asp);
+      end Decorate_Delayed_Aspect_And_Pragma;
 
       ---------------------------
       -- Insert_Delayed_Pragma --
@@ -1605,15 +1627,7 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_Depends);
 
-                  --  Decorate the aspect and pragma
-
-                  Set_Aspect_Rep_Item           (Aspect, Aitem);
-                  Set_Corresponding_Aspect      (Aitem, Aspect);
-                  Set_From_Aspect_Specification (Aitem);
-                  Set_Is_Delayed_Aspect         (Aitem);
-                  Set_Is_Delayed_Aspect         (Aspect);
-                  Set_Parent                    (Aitem, Aspect);
-
+                  Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
                   Insert_Delayed_Pragma (Aitem);
                   goto Continue;
 
@@ -1631,15 +1645,7 @@ package body Sem_Ch13 is
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Name_Global);
 
-                  --  Decorate the aspect and pragma
-
-                  Set_Aspect_Rep_Item           (Aspect, Aitem);
-                  Set_Corresponding_Aspect      (Aitem, Aspect);
-                  Set_From_Aspect_Specification (Aitem);
-                  Set_Is_Delayed_Aspect         (Aitem);
-                  Set_Is_Delayed_Aspect         (Aspect);
-                  Set_Parent                    (Aitem, Aspect);
-
+                  Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
                   Insert_Delayed_Pragma (Aitem);
                   goto Continue;
 
@@ -1739,7 +1745,7 @@ package body Sem_Ch13 is
                --  required pragma placement. The processing for the pragmas
                --  takes care of the required delay.
 
-               when Pre_Post_Aspects => declare
+               when Pre_Post_Aspects => Pre_Post : declare
                   Pname : Name_Id;
 
                begin
@@ -1816,7 +1822,7 @@ package body Sem_Ch13 is
 
                   Insert_Delayed_Pragma (Aitem);
                   goto Continue;
-               end;
+               end Pre_Post;
 
                --  Test_Case
 
@@ -1889,79 +1895,16 @@ package body Sem_Ch13 is
 
                --  Contract_Cases
 
-               when Aspect_Contract_Cases => Contract_Cases : declare
-                  Case_Guard  : Node_Id;
-                  Extra       : Node_Id;
-                  Others_Seen : Boolean := False;
-                  Post_Case   : Node_Id;
-
-               begin
-                  if Nkind (Parent (N)) = N_Compilation_Unit then
-                     Error_Msg_Name_1 := Nam;
-                     Error_Msg_N ("incorrect placement of aspect `%`", E);
-                     goto Continue;
-                  end if;
-
-                  if Nkind (Expr) /= N_Aggregate then
-                     Error_Msg_Name_1 := Nam;
-                     Error_Msg_NE
-                       ("wrong syntax for aspect `%` for &", Id, E);
-                     goto Continue;
-                  end if;
-
-                  --  Verify the legality of individual post cases
-
-                  Post_Case := First (Component_Associations (Expr));
-                  while Present (Post_Case) loop
-                     if Nkind (Post_Case) /= N_Component_Association then
-                        Error_Msg_N ("wrong syntax in post case", Post_Case);
-                        goto Continue;
-                     end if;
-
-                     --  Each post case must have exactly one case guard
-
-                     Case_Guard := First (Choices (Post_Case));
-                     Extra      := Next (Case_Guard);
-
-                     if Present (Extra) then
-                        Error_Msg_N
-                          ("post case may have only one case guard", Extra);
-                        goto Continue;
-                     end if;
-
-                     --  Check the placement of "others" (if available)
-
-                     if Nkind (Case_Guard) = N_Others_Choice then
-                        if Others_Seen then
-                           Error_Msg_Name_1 := Nam;
-                           Error_Msg_N
-                             ("only one others choice allowed in aspect %",
-                              Case_Guard);
-                           goto Continue;
-                        else
-                           Others_Seen := True;
-                        end if;
-
-                     elsif Others_Seen then
-                        Error_Msg_Name_1 := Nam;
-                        Error_Msg_N
-                          ("others must be the last choice in aspect %", N);
-                        goto Continue;
-                     end if;
-
-                     Next (Post_Case);
-                  end loop;
-
-                  --  Transform the aspect into a pragma
-
+               when Aspect_Contract_Cases =>
                   Make_Aitem_Pragma
                     (Pragma_Argument_Associations => New_List (
                        Make_Pragma_Argument_Association (Loc,
                          Expression => Relocate_Node (Expr))),
                      Pragma_Name                  => Nam);
 
-                  Delay_Required := False;
-               end Contract_Cases;
+                  Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+                  Insert_Delayed_Pragma (Aitem);
+                  goto Continue;
 
                --  Case 5: Special handling for aspects with an optional
                --  boolean argument.
@@ -1970,8 +1913,6 @@ package body Sem_Ch13 is
                --  generated yet because the evaluation of the boolean needs
                --  to be delayed till the freeze point.
 
-               --  Boolwn_Aspects
-
                when Boolean_Aspects      |
                     Library_Unit_Aspects =>
 
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index 3751ead0970..ac53a767b0e 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -64,7 +64,6 @@ with Sem_Dist; use Sem_Dist;
 with Sem_Elim; use Sem_Elim;
 with Sem_Eval; use Sem_Eval;
 with Sem_Mech; use Sem_Mech;
-with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
 with Sem_Smem; use Sem_Smem;
 with Sem_Type; use Sem_Type;
@@ -2181,59 +2180,25 @@ package body Sem_Ch3 is
          D := Next_Node;
       end loop;
 
-      --  One more thing to do, we need to scan the declarations to check
-      --  for any precondition/postcondition pragmas (Pre/Post aspects have
-      --  by this stage been converted into corresponding pragmas). It is
-      --  at this point that we analyze the expressions in such pragmas,
-      --  to implement the delayed visibility requirement.
+      --  One more thing to do, we need to scan the declarations to check for
+      --  any precondition/postcondition pragmas (Pre/Post aspects have by this
+      --  stage been converted into corresponding pragmas). It is at this point
+      --  that we analyze the expressions in such pragmas, to implement the
+      --  delayed visibility requirement.
 
       declare
-         Decl : Node_Id;
-         Spec : Node_Id;
-         Sent : Entity_Id;
-         Prag : Node_Id;
+         Decl      : Node_Id;
+         Subp_Decl : Node_Id;
+         Subp_Id   : Entity_Id;
 
       begin
          Decl := First (L);
          while Present (Decl) loop
-            if Nkind (Original_Node (Decl)) = N_Subprogram_Declaration then
-               Spec := Specification (Original_Node (Decl));
-               Sent := Defining_Unit_Name (Spec);
+            Subp_Decl := Original_Node (Decl);
 
-               --  Analyze preconditions and postconditions
-
-               Prag := Pre_Post_Conditions (Contract (Sent));
-               while Present (Prag) loop
-                  Analyze_PPC_In_Decl_Part (Prag, Sent);
-                  Prag := Next_Pragma (Prag);
-               end loop;
-
-               --  Analyze contract-cases and test-cases
-
-               Prag := Contract_Test_Cases (Contract (Sent));
-               while Present (Prag) loop
-                  Analyze_CTC_In_Decl_Part (Prag, Sent);
-                  Prag := Next_Pragma (Prag);
-               end loop;
-
-               --  Analyze classification pragmas
-
-               Prag := Classifications (Contract (Sent));
-               while Present (Prag) loop
-                  if Pragma_Name (Prag) = Name_Depends then
-                     Analyze_Depends_In_Decl_Part (Prag);
-                  else
-                     pragma Assert (Pragma_Name (Prag) = Name_Global);
-                     Analyze_Global_In_Decl_Part (Prag);
-                  end if;
-
-                  Prag := Next_Pragma (Prag);
-               end loop;
-
-               --  At this point, entities have been attached to identifiers.
-               --  This is required to be able to detect suspicious contracts.
-
-               Check_Subprogram_Contract (Sent);
+            if Nkind (Subp_Decl) = N_Subprogram_Declaration then
+               Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
+               Analyze_Subprogram_Contract (Subp_Id);
             end if;
 
             Next (Decl);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 42c9fb2c115..385076b5693 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3320,6 +3320,281 @@ package body Sem_Ch6 is
       end;
    end Analyze_Subprogram_Body_Helper;
 
+   ---------------------------------
+   -- Analyze_Subprogram_Contract --
+   ---------------------------------
+
+   procedure Analyze_Subprogram_Contract (Subp : Entity_Id) is
+      Result_Seen : Boolean := False;
+      --  A flag which keeps track of whether at least one postcondition or
+      --  contract-case mentions attribute 'Result (set True if so).
+
+      procedure Check_Result_And_Post_State
+        (Prag      : Node_Id;
+         Error_Nod : in out Node_Id);
+      --  Determine whether pragma Prag mentions attribute 'Result and whether
+      --  the pragma contains an expression that evaluates differently in pre-
+      --  and post-state. Prag is a postcondition or a contract-cases pragma.
+      --  Error_Nod denotes the proper error node.
+
+      ---------------------------------
+      -- Check_Result_And_Post_State --
+      ---------------------------------
+
+      procedure Check_Result_And_Post_State
+        (Prag      : Node_Id;
+         Error_Nod : in out Node_Id)
+      is
+         procedure Check_Expression (Expr : Node_Id);
+         --  Perform the 'Result and post-state checks on a given expression
+
+         function Is_Function_Result (N : Node_Id) return Traverse_Result;
+         --  Attempt to find attribute 'Result in a subtree denoted by N
+
+         function Is_Trivial_Boolean (N : Node_Id) return Boolean;
+         --  Determine whether source node N denotes "True" or "False"
+
+         function Mentions_Post_State (N : Node_Id) return Boolean;
+         --  Determine whether a subtree denoted by N mentions any construct
+         --  that denotes a post-state.
+
+         procedure Check_Function_Result is
+           new Traverse_Proc (Is_Function_Result);
+
+         ----------------------
+         -- Check_Expression --
+         ----------------------
+
+         procedure Check_Expression (Expr : Node_Id) is
+         begin
+            if not Is_Trivial_Boolean (Expr) then
+               Check_Function_Result (Expr);
+
+               if not Mentions_Post_State (Expr) then
+                  if Pragma_Name (Prag) = Name_Contract_Cases then
+                     Error_Msg_N
+                       ("contract case refers only to pre-state?T?", Expr);
+                  else
+                     Error_Msg_N
+                       ("postcondition refers only to pre-state?T?", Prag);
+                  end if;
+               end if;
+            end if;
+         end Check_Expression;
+
+         ------------------------
+         -- Is_Function_Result --
+         ------------------------
+
+         function Is_Function_Result (N : Node_Id) return Traverse_Result is
+         begin
+            if Nkind (N) = N_Attribute_Reference
+              and then Attribute_Name (N) = Name_Result
+            then
+               Result_Seen := True;
+               return Abandon;
+
+            --  Continue the traversal
+
+            else
+               return OK;
+            end if;
+         end Is_Function_Result;
+
+         ------------------------
+         -- Is_Trivial_Boolean --
+         ------------------------
+
+         function Is_Trivial_Boolean (N : Node_Id) return Boolean is
+         begin
+            return
+              Comes_From_Source (N)
+                and then Is_Entity_Name (N)
+                and then (Entity (N) = Standard_True
+                            or else Entity (N) = Standard_False);
+         end Is_Trivial_Boolean;
+
+         -------------------------
+         -- Mentions_Post_State --
+         -------------------------
+
+         function Mentions_Post_State (N : Node_Id) return Boolean is
+            Post_State_Seen : Boolean := False;
+
+            function Is_Post_State (N : Node_Id) return Traverse_Result;
+            --  Attempt to find a construct that denotes a post-state. If this
+            --  is the case, set flag Post_State_Seen.
+
+            -------------------
+            -- Is_Post_State --
+            -------------------
+
+            function Is_Post_State (N : Node_Id) return Traverse_Result is
+               Ent : Entity_Id;
+
+            begin
+               if Nkind_In (N, N_Explicit_Dereference, N_Function_Call) then
+                  Post_State_Seen := True;
+                  return Abandon;
+
+               elsif Nkind_In (N, N_Expanded_Name, N_Identifier) then
+                  Ent := Entity (N);
+
+                  if No (Ent) or else Ekind (Ent) in Assignable_Kind then
+                     Post_State_Seen := True;
+                     return Abandon;
+                  end if;
+
+               elsif Nkind (N) = N_Attribute_Reference then
+                  if Attribute_Name (N) = Name_Old then
+                     return Skip;
+                  elsif Attribute_Name (N) = Name_Result then
+                     Post_State_Seen := True;
+                     return Abandon;
+                  end if;
+               end if;
+
+               return OK;
+            end Is_Post_State;
+
+            procedure Find_Post_State is new Traverse_Proc (Is_Post_State);
+
+         --  Start of processing for Mentions_Post_State
+
+         begin
+            Find_Post_State (N);
+            return Post_State_Seen;
+         end Mentions_Post_State;
+
+         --  Local variables
+
+         Expr  : constant Node_Id :=
+                   Expression (First (Pragma_Argument_Associations (Prag)));
+         Nam   : constant Name_Id := Pragma_Name (Prag);
+         CCase : Node_Id;
+
+      --  Start of processing for Check_Result_And_Post_State
+
+      begin
+         if No (Error_Nod) then
+            Error_Nod := Prag;
+         end if;
+
+         --  Examine all consequences
+
+         if Nam = Name_Contract_Cases then
+            CCase := First (Component_Associations (Expr));
+            while Present (CCase) loop
+               Check_Expression (Expression (CCase));
+
+               Next (CCase);
+            end loop;
+
+         --  Examine the expression of a postcondition
+
+         else
+            pragma Assert (Nam = Name_Postcondition);
+            Check_Expression (Expr);
+         end if;
+      end Check_Result_And_Post_State;
+
+      --  Local variables
+
+      Items       : constant Node_Id := Contract (Subp);
+      Error_CCase : Node_Id;
+      Error_Post  : Node_Id;
+      Prag        : Node_Id;
+
+   --  Start of processing for Analyze_Subprogram_Contract
+
+   begin
+      Error_CCase := Empty;
+      Error_Post  := Empty;
+
+      if Present (Items) then
+
+         --  Analyze pre- and postconditions
+
+         Prag := Pre_Post_Conditions (Items);
+         while Present (Prag) loop
+            Analyze_PPC_In_Decl_Part (Prag, Subp);
+
+            --  Verify whether a postcondition mentions attribute 'Result and
+            --  its expression introduces a post-state.
+
+            if Warn_On_Suspicious_Contract
+              and then Pragma_Name (Prag) = Name_Postcondition
+            then
+               Check_Result_And_Post_State (Prag, Error_Post);
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+
+         --  Analyze contract-cases and test-cases
+
+         Prag := Contract_Test_Cases (Items);
+         while Present (Prag) loop
+            if Pragma_Name (Prag) = Name_Contract_Cases then
+               Analyze_Contract_Cases_In_Decl_Part (Prag);
+
+               --  Verify whether contract-cases mention attribute 'Result and
+               --  its expression introduces a post-state. Perform the check
+               --  only when the pragma is legal.
+
+               if Warn_On_Suspicious_Contract
+                 and then not Error_Posted (Prag)
+               then
+                  Check_Result_And_Post_State (Prag, Error_CCase);
+               end if;
+
+            else
+               pragma Assert (Pragma_Name (Prag) = Name_Test_Case);
+               Analyze_Test_Case_In_Decl_Part (Prag, Subp);
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+
+         --  Analyze classification pragmas
+
+         Prag := Classifications (Contract (Subp));
+         while Present (Prag) loop
+            if Pragma_Name (Prag) = Name_Depends then
+               Analyze_Depends_In_Decl_Part (Prag);
+            else
+               pragma Assert (Pragma_Name (Prag) = Name_Global);
+               Analyze_Global_In_Decl_Part (Prag);
+            end if;
+
+            Prag := Next_Pragma (Prag);
+         end loop;
+      end if;
+
+      --  Emit an error when none of the postconditions or contract-cases
+      --  mention attribute 'Result in the context of a function.
+
+      if Warn_On_Suspicious_Contract
+        and then Ekind_In (Subp, E_Function, E_Generic_Function)
+        and then not Result_Seen
+      then
+         if Present (Error_Post) and then Present (Error_CCase) then
+            Error_Msg_N
+              ("neither function postcondition nor contract cases mention "
+               & "result?T?", Error_Post);
+
+         elsif Present (Error_Post) then
+            Error_Msg_N
+              ("function postcondition does not mention result?T?",
+               Error_Post);
+
+         elsif Present (Error_CCase) then
+            Error_Msg_N
+              ("contract cases do not mention result?T?", Error_CCase);
+         end if;
+      end if;
+   end Analyze_Subprogram_Contract;
+
    ------------------------------------
    -- Analyze_Subprogram_Declaration --
    ------------------------------------
@@ -7035,344 +7310,6 @@ package body Sem_Ch6 is
       end if;
    end Check_Returns;
 
-   -------------------------------
-   -- Check_Subprogram_Contract --
-   -------------------------------
-
-   procedure Check_Subprogram_Contract (Spec_Id : Entity_Id) is
-
-      --  Code is currently commented out as, in some cases, it causes crashes
-      --  because Direct_Primitive_Operations is not available for a private
-      --  type. This may cause more warnings to be issued than necessary. See
-      --  below for the intended use of this variable. ???
-
---        Inherited : constant Subprogram_List :=
---                      Inherited_Subprograms (Spec_Id);
---        --  List of subprograms inherited by this subprogram
-
-      --  We ignore postconditions "True" or "False" and contract-cases which
-      --  have similar consequence expressions, which we call "trivial", when
-      --  issuing warnings, since these postconditions and contract-cases
-      --  purposedly ignore the post-state.
-
-      Last_Postcondition : Node_Id := Empty;
-      --  Last non-trivial postcondition on the subprogram, or else Empty if
-      --  either no non-trivial postcondition or only inherited postconditions.
-
-      Last_Contract_Cases : Node_Id := Empty;
-      --  Last non-trivial contract-cases on the subprogram, or else Empty
-
-      Attribute_Result_Mentioned : Boolean := False;
-      --  True if 'Result used in a non-trivial postcondition or contract-cases
-
-      No_Warning_On_Some_Postcondition : Boolean := False;
-      --  True if there is a non-trivial postcondition or contract-cases
-      --  without a corresponding warning.
-
-      Post_State_Mentioned : Boolean := False;
-      --  True if expression mentioned in a postcondition or contract-cases
-      --  can have a different value in the post-state than in the pre-state.
-
-      function Check_Attr_Result (N : Node_Id) return Traverse_Result;
-      --  Check if N is a reference to the attribute 'Result, and if so set
-      --  Attribute_Result_Mentioned and return Abandon. Otherwise return OK.
-
-      function Check_Post_State (N : Node_Id) return Traverse_Result;
-      --  Check whether the value of evaluating N can be different in the
-      --  post-state, compared to the same evaluation in the pre-state, and
-      --  if so set Post_State_Mentioned and return Abandon. Return Skip on
-      --  reference to attribute 'Old, in order to ignore its prefix, which
-      --  is precisely evaluated in the pre-state. Otherwise return OK.
-
-      function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean;
-      --  Return True if node N is trivially "True" or "False", and it comes
-      --  from source. In particular, nodes that are statically known "True" or
-      --  "False" by the compiler but not written as such in source code are
-      --  not considered as trivial.
-
-      procedure Process_Contract_Cases (Spec : Node_Id);
-      --  This processes the Contract_Test_Cases from Spec, processing any
-      --  contract case from the list. The caller has checked that list
-      --  Contract_Test_Cases is non-Empty.
-
-      procedure Process_Post_Conditions (Spec : Node_Id; Class : Boolean);
-      --  This processes the Pre_Post_Conditions from Spec, processing any
-      --  postcondition from the list. If Class is True, then only
-      --  postconditions marked with Class_Present are considered. The
-      --  caller has checked that Pre_Post_Conditions is non-Empty.
-
-      function Find_Attribute_Result is new Traverse_Func (Check_Attr_Result);
-
-      function Find_Post_State is new Traverse_Func (Check_Post_State);
-
-      -----------------------
-      -- Check_Attr_Result --
-      -----------------------
-
-      function Check_Attr_Result (N : Node_Id) return Traverse_Result is
-      begin
-         if Nkind (N) = N_Attribute_Reference
-           and then Get_Attribute_Id (Attribute_Name (N)) = Attribute_Result
-         then
-            Attribute_Result_Mentioned := True;
-            return Abandon;
-         else
-            return OK;
-         end if;
-      end Check_Attr_Result;
-
-      ----------------------
-      -- Check_Post_State --
-      ----------------------
-
-      function Check_Post_State (N : Node_Id) return Traverse_Result is
-         Found : Boolean := False;
-
-      begin
-         case Nkind (N) is
-            when N_Function_Call        |
-                 N_Explicit_Dereference =>
-               Found := True;
-
-            when N_Identifier    |
-                 N_Expanded_Name =>
-
-               declare
-                  E : constant Entity_Id := Entity (N);
-
-               begin
-                  --  ???Quantified expressions get analyzed later, so E can
-                  --  be empty at this point. In this case, we suppress the
-                  --  warning, just in case E is assignable. It seems better to
-                  --  have false negatives than false positives. At some point,
-                  --  we should make the warning more accurate, either by
-                  --  analyzing quantified expressions earlier, or moving
-                  --  this processing later.
-
-                  if No (E)
-                    or else
-                      (Is_Entity_Name (N)
-                        and then Ekind (E) in Assignable_Kind)
-                  then
-                     Found := True;
-                  end if;
-               end;
-
-            when N_Attribute_Reference =>
-               case Get_Attribute_Id (Attribute_Name (N)) is
-                  when Attribute_Old =>
-                     return Skip;
-                  when Attribute_Result =>
-                     Found := True;
-                  when others =>
-                     null;
-               end case;
-
-            when others =>
-               null;
-         end case;
-
-         if Found then
-            Post_State_Mentioned := True;
-            return Abandon;
-         else
-            return OK;
-         end if;
-      end Check_Post_State;
-
-      --------------------------------
-      -- Is_Trivial_Post_Or_Ensures --
-      --------------------------------
-
-      function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean is
-      begin
-         return Is_Entity_Name (N)
-           and then (Entity (N) = Standard_True
-                       or else
-                     Entity (N) = Standard_False)
-           and then Comes_From_Source (N);
-      end Is_Trivial_Post_Or_Ensures;
-
-      ----------------------------
-      -- Process_Contract_Cases --
-      ----------------------------
-
-      procedure Process_Contract_Cases (Spec : Node_Id) is
-         Prag       : Node_Id;
-         Aggr       : Node_Id;
-         Conseq     : Node_Id;
-         Post_Case  : Node_Id;
-
-         Ignored : Traverse_Final_Result;
-         pragma Unreferenced (Ignored);
-
-      begin
-         Prag := Contract_Test_Cases (Contract (Spec));
-         loop
-            if Pragma_Name (Prag) = Name_Contract_Cases then
-               Aggr :=
-                 Expression (First (Pragma_Argument_Associations (Prag)));
-
-               Post_Case := First (Component_Associations (Aggr));
-               while Present (Post_Case) loop
-                  Conseq := Expression (Post_Case);
-
-                  --  Ignore trivial contract-cases when consequence is "True"
-                  --  or "False".
-
-                  if not Is_Trivial_Post_Or_Ensures (Conseq) then
-                     Last_Contract_Cases := Prag;
-
-                     --  For functions, look for presence of 'Result in
-                     --  consequence expression.
-
-                     if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
-                        Ignored := Find_Attribute_Result (Conseq);
-                     end if;
-
-                     --  For each individual case, look for presence of an
-                     --  expression that could be evaluated differently in
-                     --  post-state.
-
-                     Post_State_Mentioned := False;
-                     Ignored := Find_Post_State (Conseq);
-
-                     if Post_State_Mentioned then
-                        No_Warning_On_Some_Postcondition := True;
-                     else
-                        Error_Msg_N
-                          ("contract case refers only to pre-state?T?",
-                           Conseq);
-                     end if;
-                  end if;
-
-                  Next (Post_Case);
-               end loop;
-            end if;
-
-            Prag := Next_Pragma (Prag);
-            exit when No (Prag);
-         end loop;
-      end Process_Contract_Cases;
-
-      -----------------------------
-      -- Process_Post_Conditions --
-      -----------------------------
-
-      procedure Process_Post_Conditions
-        (Spec  : Node_Id;
-         Class : Boolean)
-      is
-         Prag    : Node_Id;
-         Arg     : Node_Id;
-         Ignored : Traverse_Final_Result;
-         pragma Unreferenced (Ignored);
-
-      begin
-         Prag := Pre_Post_Conditions (Contract (Spec));
-         loop
-            Arg := First (Pragma_Argument_Associations (Prag));
-
-            --  Ignore trivial postcondition of "True" or "False"
-
-            if Pragma_Name (Prag) = Name_Postcondition
-              and then not Is_Trivial_Post_Or_Ensures (Expression (Arg))
-            then
-               --  Since pre- and post-conditions are listed in reverse order,
-               --  the first postcondition in the list is last in the source.
-
-               if not Class and then No (Last_Postcondition) then
-                  Last_Postcondition := Prag;
-               end if;
-
-               --  For functions, look for presence of 'Result in postcondition
-
-               if Ekind_In (Spec_Id, E_Function, E_Generic_Function) then
-                  Ignored := Find_Attribute_Result (Arg);
-               end if;
-
-               --  For each individual non-inherited postcondition, look
-               --  for presence of an expression that could be evaluated
-               --  differently in post-state.
-
-               if not Class then
-                  Post_State_Mentioned := False;
-                  Ignored := Find_Post_State (Arg);
-
-                  if Post_State_Mentioned then
-                     No_Warning_On_Some_Postcondition := True;
-                  else
-                     Error_Msg_N
-                       ("postcondition refers only to pre-state?T?", Prag);
-                  end if;
-               end if;
-            end if;
-
-            Prag := Next_Pragma (Prag);
-            exit when No (Prag);
-         end loop;
-      end Process_Post_Conditions;
-
-   --  Start of processing for Check_Subprogram_Contract
-
-   begin
-      if not Warn_On_Suspicious_Contract then
-         return;
-      end if;
-
-      --  Process spec postconditions
-
-      if Present (Pre_Post_Conditions (Contract (Spec_Id))) then
-         Process_Post_Conditions (Spec_Id, Class => False);
-      end if;
-
-      --  Process inherited postconditions
-
-      --  Code is currently commented out as, in some cases, it causes crashes
-      --  because Direct_Primitive_Operations is not available for a private
-      --  type. This may cause more warnings to be issued than necessary. ???
-
---        for J in Inherited'Range loop
---           if Present (Pre_Post_Conditions (Contract (Inherited (J)))) then
---              Process_Post_Conditions (Inherited (J), Class => True);
---           end if;
---        end loop;
-
-      --  Process contract cases
-
-      if Present (Contract_Test_Cases (Contract (Spec_Id))) then
-         Process_Contract_Cases (Spec_Id);
-      end if;
-
-      --  Issue warning for functions whose postcondition does not mention
-      --  'Result after all postconditions have been processed, and provided
-      --  all postconditions do not already get a warning that they only refer
-      --  to pre-state.
-
-      if Ekind_In (Spec_Id, E_Function, E_Generic_Function)
-        and then (Present (Last_Postcondition)
-                   or else Present (Last_Contract_Cases))
-        and then not Attribute_Result_Mentioned
-        and then No_Warning_On_Some_Postcondition
-      then
-         if Present (Last_Postcondition) then
-            if Present (Last_Contract_Cases) then
-               Error_Msg_N
-                 ("neither function postcondition nor "
-                  & "contract cases mention result?T?", Last_Postcondition);
-
-            else
-               Error_Msg_N
-                 ("function postcondition does not mention result?T?",
-                  Last_Postcondition);
-            end if;
-         else
-            Error_Msg_N
-              ("contract cases do not mention result?T?", Last_Contract_Cases);
-         end if;
-      end if;
-   end Check_Subprogram_Contract;
-
    ----------------------------
    -- Check_Subprogram_Order --
    ----------------------------
@@ -11578,8 +11515,6 @@ package body Sem_Ch6 is
                            Expression (First
                              (Pragma_Argument_Associations (CCs)));
          Decls         : constant List_Id := Declarations (N);
-         Multiple_PCs  : constant Boolean :=
-                           List_Length (Component_Associations (Aggr)) > 1;
          Case_Guard    : Node_Id;
          CG_Checks     : Node_Id;
          CG_Stmts      : List_Id;
@@ -11589,6 +11524,7 @@ package body Sem_Ch6 is
          Error_Decls   : List_Id;
          Flag          : Entity_Id;
          Msg_Str       : Entity_Id;
+         Multiple_PCs  : Boolean;
          Others_Flag   : Entity_Id := Empty;
          Post_Case     : Node_Id;
 
@@ -11600,8 +11536,15 @@ package body Sem_Ch6 is
 
          if Is_Ignored (CCs) then
             return;
+
+         --  Guard against malformed contract cases
+
+         elsif Nkind (Aggr) /= N_Aggregate then
+            return;
          end if;
 
+         Multiple_PCs := List_Length (Component_Associations (Aggr)) > 1;
+
          --  Create the counter which tracks the number of case guards that
          --  evaluate to True.
 
diff --git a/gcc/ada/sem_ch6.ads b/gcc/ada/sem_ch6.ads
index a0df51ef21e..0799adc1849 100644
--- a/gcc/ada/sem_ch6.ads
+++ b/gcc/ada/sem_ch6.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -46,6 +46,10 @@ package Sem_Ch6 is
    procedure Analyze_Subprogram_Declaration          (N : Node_Id);
    procedure Analyze_Subprogram_Body                 (N : Node_Id);
 
+   procedure Analyze_Subprogram_Contract (Subp : Entity_Id);
+   --  Analyze all delayed aspects chained on the contract of subprogram Subp
+   --  as if they appeared at the end of a declarative region.
+
    function Analyze_Subprogram_Specification (N : Node_Id) return Entity_Id;
    --  Analyze subprogram specification in both subprogram declarations
    --  and body declarations. Returns the defining entity for the
@@ -139,10 +143,6 @@ package Sem_Ch6 is
    --  type-conformant subprogram that becomes hidden by the new subprogram.
    --  Is_Primitive indicates whether the subprogram is primitive.
 
-   procedure Check_Subprogram_Contract (Spec_Id : Entity_Id);
-   --  Spec_Id is the spec entity for a subprogram. This routine issues
-   --  warnings on suspicious contracts if Warn_On_Suspicious_Contract is set.
-
    procedure Check_Subtype_Conformant
      (New_Id                   : Entity_Id;
       Old_Id                   : Entity_Id;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 835e8197c67..9339d490c97 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -181,6 +181,13 @@ package body Sem_Prag is
    --  to Uppercase or Lowercase, then a new string literal with appropriate
    --  casing is constructed.
 
+   function Find_Related_Subprogram
+     (Prag             : Node_Id;
+      Check_Duplicates : Boolean := False) return Node_Id;
+   --  Find the declaration of the related subprogram subject to pragma Prag.
+   --  If flag Check_Duplicates is set, the routine emits errors concerning
+   --  duplicate pragmas.
+
    function Get_Base_Subprogram (Def_Id : Entity_Id) return Entity_Id;
    --  If Def_Id refers to a renamed subprogram, then the base subprogram (the
    --  original one, following the renaming chain) is returned. Otherwise the
@@ -213,10 +220,12 @@ package body Sem_Prag is
    --  pragma in the source program, a breakpoint on rv catches this place in
    --  the source, allowing convenient stepping to the point of interest.
 
-   function Requires_Profile_Installation (Subp : Node_Id) return Boolean;
+   function Requires_Profile_Installation
+     (Prag : Node_Id;
+      Subp : Node_Id) return Boolean;
    --  Subsidiary routine to the analysis of pragma Depends and pragma Global.
    --  Determine whether the profile of subprogram Subp must be installed into
-   --  visibility to access its formals.
+   --  visibility to access its formals from pragma Prag.
 
    procedure Set_Unit_Name (N : Node_Id; With_Item : Node_Id);
    --  Place semantic information on the argument of an Elaborate/Elaborate_All
@@ -282,33 +291,57 @@ package body Sem_Prag is
       end if;
    end Adjust_External_Name_Case;
 
-   ------------------------------
-   -- Analyze_CTC_In_Decl_Part --
-   ------------------------------
+   -----------------------------------------
+   -- Analyze_Contract_Cases_In_Decl_Part --
+   -----------------------------------------
 
-   procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id) is
+   procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id) is
+      Others_Seen : Boolean := False;
 
-      procedure Analyze_Contract_Cases (Aggr : Node_Id);
-      --  Pre-analyze the guard and consequence expressions of a Contract_Cases
-      --  pragma/aspect aggregate expression.
+      procedure Analyze_Contract_Case (CCase : Node_Id);
+      --  Verify the legality of a single contract case
 
-      ----------------------------
-      -- Analyze_Contract_Cases --
-      ----------------------------
+      ---------------------------
+      -- Analyze_Contract_Case --
+      ---------------------------
 
-      procedure Analyze_Contract_Cases (Aggr : Node_Id) is
-         Case_Guard : Node_Id;
-         Conseq     : Node_Id;
-         Post_Case  : Node_Id;
+      procedure Analyze_Contract_Case (CCase : Node_Id) is
+         Case_Guard  : Node_Id;
+         Conseq      : Node_Id;
+         Extra_Guard : Node_Id;
 
       begin
-         Post_Case := First (Component_Associations (Aggr));
-         while Present (Post_Case) loop
-            Case_Guard := First (Choices (Post_Case));
-            Conseq     := Expression (Post_Case);
+         if Nkind (CCase) = N_Component_Association then
+            Case_Guard := First (Choices (CCase));
+            Conseq     := Expression (CCase);
+
+            --  Each contract case must have exactly one case guard
 
-            --  Preanalyze the boolean expression, we treat this as a spec
-            --  expression (i.e. similar to a default expression).
+            Extra_Guard := Next (Case_Guard);
+
+            if Present (Extra_Guard) then
+               Error_Msg_N
+                 ("contract case may have only one case guard", Extra_Guard);
+            end if;
+
+            --  Check the placement of "others" (if available)
+
+            if Nkind (Case_Guard) = N_Others_Choice then
+               if Others_Seen then
+                  Error_Msg_N
+                    ("only one others choice allowed in aspect Contract_Cases",
+                     Case_Guard);
+               else
+                  Others_Seen := True;
+               end if;
+
+            elsif Others_Seen then
+               Error_Msg_N
+                 ("others must be the last choice in aspect Contract_Cases",
+                  N);
+            end if;
+
+            --  Preanalyze the case guard and consequence
 
             if Nkind (Case_Guard) /= N_Others_Choice then
                Preanalyze_Assert_Expression (Case_Guard, Standard_Boolean);
@@ -316,46 +349,64 @@ package body Sem_Prag is
 
             Preanalyze_Assert_Expression (Conseq, Standard_Boolean);
 
-            Next (Post_Case);
-         end loop;
-      end Analyze_Contract_Cases;
+         --  The contract case is malformed
 
-   --  Start of processing for Analyze_CTC_In_Decl_Part
+         else
+            Error_Msg_N ("wrong syntax in contract case", CCase);
+         end if;
+      end Analyze_Contract_Case;
+
+      --  Local variables
+
+      Arg1      : constant Node_Id := First (Pragma_Argument_Associations (N));
+      All_Cases : Node_Id;
+      CCase     : Node_Id;
+      Subp_Decl : Node_Id;
+      Subp_Id   : Entity_Id;
+
+   --  Start of processing for Analyze_Contract_Cases_In_Decl_Part
 
    begin
-      --  Install formals and push subprogram spec onto scope stack so that we
-      --  can see the formals from the pragma.
+      Set_Analyzed (N);
 
-      Push_Scope (S);
-      Install_Formals (S);
+      Subp_Decl := Find_Related_Subprogram (N);
+      Subp_Id   := Defining_Unit_Name (Specification (Subp_Decl));
+      All_Cases := Expression (Arg1);
 
-      --  Preanalyze the boolean expressions, we treat these as spec
-      --  expressions (i.e. similar to a default expression).
+      --  Multiple contract cases appear in aggregate form
 
-      if Pragma_Name (N) = Name_Test_Case then
-         Preanalyze_CTC_Args
-           (N,
-            Get_Requires_From_CTC_Pragma (N),
-            Get_Ensures_From_CTC_Pragma (N));
+      if Nkind (All_Cases) = N_Aggregate then
+         if No (Component_Associations (All_Cases)) then
+            Error_Msg_N ("wrong syntax for aspect Contract_Cases", N);
 
-      else
-         pragma Assert (Pragma_Name (N) = Name_Contract_Cases);
-         Analyze_Contract_Cases
-           (Expression (First (Pragma_Argument_Associations (N))));
+         --  Individual contract cases appear as component associations
 
-         --  In ASIS mode, for a pragma generated from a source aspect, also
-         --  analyze the original aspect expression.
+         else
+            --  Ensure that the formal parameters are visible when analyzing
+            --  all clauses. This falls out of the general rule of aspects
+            --  pertaining to subprogram declarations. Skip the installation
+            --  for subprogram bodies because the formals are already visible.
 
-         if ASIS_Mode and then Present (Corresponding_Aspect (N)) then
-            Analyze_Contract_Cases (Expression (Corresponding_Aspect (N)));
-         end if;
-      end if;
+            if Requires_Profile_Installation (N, Subp_Decl) then
+               Push_Scope (Subp_Id);
+               Install_Formals (Subp_Id);
+            end if;
 
-      --  Remove the subprogram from the scope stack now that the pre-analysis
-      --  of the expressions in the contract case or test case is done.
+            CCase := First (Component_Associations (All_Cases));
+            while Present (CCase) loop
+               Analyze_Contract_Case (CCase);
+               Next (CCase);
+            end loop;
 
-      End_Scope;
-   end Analyze_CTC_In_Decl_Part;
+            if Requires_Profile_Installation (N, Subp_Decl) then
+               End_Scope;
+            end if;
+         end if;
+
+      else
+         Error_Msg_N ("wrong syntax for aspect Contract_Cases", N);
+      end if;
+   end Analyze_Contract_Cases_In_Decl_Part;
 
    ----------------------------------
    -- Analyze_Depends_In_Decl_Part --
@@ -1358,7 +1409,7 @@ package body Sem_Prag is
          --  to subprogram declarations. Skip the installation for subprogram
          --  bodies because the formals are already visible.
 
-         if Requires_Profile_Installation (Subp_Decl) then
+         if Requires_Profile_Installation (N, Subp_Decl) then
             Push_Scope (Subp_Id);
             Install_Formals (Subp_Id);
          end if;
@@ -1389,7 +1440,7 @@ package body Sem_Prag is
             Next (Clause);
          end loop;
 
-         if Requires_Profile_Installation (Subp_Decl) then
+         if Requires_Profile_Installation (N, Subp_Decl) then
             End_Scope;
          end if;
 
@@ -1713,14 +1764,14 @@ package body Sem_Prag is
          --  item. This falls out of the general rule of aspects pertaining to
          --  subprogram declarations.
 
-         if Requires_Profile_Installation (Subp_Decl) then
+         if Requires_Profile_Installation (N, Subp_Decl) then
             Push_Scope (Subp_Id);
             Install_Formals (Subp_Id);
          end if;
 
          Analyze_Global_List (List);
 
-         if Requires_Profile_Installation (Subp_Decl) then
+         if Requires_Profile_Installation (N, Subp_Decl) then
             End_Scope;
          end if;
       end if;
@@ -10049,204 +10100,46 @@ package body Sem_Prag is
          --  CONSEQUENCE ::= boolean_EXPRESSION
 
          when Pragma_Contract_Cases => Contract_Cases : declare
-            Others_Seen : Boolean := False;
-
-            procedure Analyze_Contract_Case (Contract_Case : Node_Id);
-            --  Verify the legality of a single contract case
-
-            procedure Chain_Contract_Cases (Subp_Id : Entity_Id);
-            --  Chain pragma Contract_Cases to the contract of a subprogram.
-            --  Subp_Id is the related subprogram.
-
-            ---------------------------
-            -- Analyze_Contract_Case --
-            ---------------------------
-
-            procedure Analyze_Contract_Case (Contract_Case : Node_Id) is
-               Case_Guard  : Node_Id;
-               Extra_Guard : Node_Id;
-
-            begin
-               if Nkind (Contract_Case) = N_Component_Association then
-                  Case_Guard := First (Choices (Contract_Case));
-
-                  --  Each contract case must have exactly on case guard
-
-                  Extra_Guard := Next (Case_Guard);
-
-                  if Present (Extra_Guard) then
-                     Error_Pragma_Arg
-                       ("contract case may have only one case guard",
-                        Extra_Guard);
-                  end if;
-
-                  --  Check the placement of "others" (if available)
-
-                  if Nkind (Case_Guard) = N_Others_Choice then
-                     if Others_Seen then
-                        Error_Pragma_Arg
-                          ("only one others choice allowed in pragma %",
-                           Case_Guard);
-                     else
-                        Others_Seen := True;
-                     end if;
-
-                  elsif Others_Seen then
-                     Error_Pragma_Arg
-                       ("others must be the last choice in pragma %", N);
-                  end if;
-
-               --  The contract case is malformed
-
-               else
-                  Error_Pragma_Arg
-                    ("wrong syntax in contract case", Contract_Case);
-               end if;
-            end Analyze_Contract_Case;
-
-            --------------------------
-            -- Chain_Contract_Cases --
-            --------------------------
-
-            procedure Chain_Contract_Cases (Subp_Id : Entity_Id) is
-               CTC : Node_Id;
-
-            begin
-               Check_Duplicate_Pragma (Subp_Id);
-               CTC := Contract_Test_Cases (Contract (Subp_Id));
-               while Present (CTC) loop
-                  if Chars (Pragma_Identifier (CTC)) = Pname then
-                     Error_Msg_Name_1 := Pname;
-                     Error_Msg_Sloc   := Sloc (CTC);
-
-                     if From_Aspect_Specification (CTC) then
-                        Error_Msg_NE
-                          ("aspect% for & previously given#", N, Subp_Id);
-                     else
-                        Error_Msg_NE
-                          ("pragma% for & duplicates pragma#", N, Subp_Id);
-                     end if;
-
-                     raise Pragma_Exit;
-                  end if;
-
-                  CTC := Next_Pragma (CTC);
-               end loop;
-
-               --  Prepend pragma Contract_Cases to the contract
-
-               Add_Contract_Item (N, Subp_Id);
-            end Chain_Contract_Cases;
-
-            --  Local variables
-
-            Context       : constant Node_Id := Parent (N);
-            All_Cases     : Node_Id;
-            Decl          : Node_Id;
-            Contract_Case : Node_Id;
-            Subp_Decl     : Node_Id;
-            Subp_Id       : Entity_Id;
-
-         --  Start of processing for Contract_Cases
+            Subp_Decl : Node_Id;
+            Subp_Id   : Entity_Id;
 
          begin
             GNAT_Pragma;
+            S14_Pragma;
             Check_Arg_Count (1);
 
-            --  Check the placement of the pragma
+            --  Ensure the proper placement of the pragma. Contract_Cases must
+            --  be associated with a subprogram declaration or a body that acts
+            --  as a spec.
+
+            Subp_Decl := Find_Related_Subprogram (N, Check_Duplicates => True);
 
-            if not Is_List_Member (N) then
+            if Nkind (Subp_Decl) /= N_Subprogram_Declaration
+              and then (Nkind (Subp_Decl) /= N_Subprogram_Body
+                         or else not Acts_As_Spec (Subp_Decl))
+            then
                Pragma_Misplaced;
+               return;
             end if;
 
-            --  Aspect/pragma Contract_Cases may be associated with a library
-            --  level subprogram.
-
-            if Nkind (Context) = N_Compilation_Unit_Aux then
-               Subp_Decl := Unit (Parent (Context));
-
-               if not Nkind_In (Subp_Decl, N_Generic_Subprogram_Declaration,
-                                           N_Subprogram_Declaration)
-               then
-                  Pragma_Misplaced;
-               end if;
-
-               Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
-
-            --  The aspect/pragma appears in a subprogram body. The placement
-            --  is legal when the body acts as a spec.
-
-            elsif Nkind (Context) = N_Subprogram_Body then
-               Subp_Id := Defining_Unit_Name (Specification (Context));
-
-               if not Acts_As_Spec (Context) then
-                  Error_Pragma
-                    ("pragma % may not appear in a subprogram body that acts "
-                     & "as completion");
-               end if;
-
-            --  Nested subprogram case, the aspect/pragma must apply to the
-            --  subprogram spec.
-
-            else
-               Decl := N;
-               while Present (Prev (Decl)) loop
-                  Decl := Prev (Decl);
-
-                  if Nkind (Decl) in N_Generic_Declaration then
-                     Subp_Decl := Decl;
-                  else
-                     Subp_Decl := Original_Node (Decl);
-                  end if;
-
-                  --  Skip prior pragmas
-
-                  if Nkind (Subp_Decl) = N_Pragma then
-                     null;
-
-                  --  Skip internally generated code
-
-                  elsif not Comes_From_Source (Subp_Decl) then
-                     null;
-
-                  --  We have found the related subprogram
-
-                  elsif Nkind_In (Subp_Decl, N_Generic_Subprogram_Declaration,
-                                             N_Subprogram_Declaration)
-                  then
-                     exit;
-
-                  else
-                     Pragma_Misplaced;
-                  end if;
-               end loop;
-
-               Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
-            end if;
+            Subp_Id := Defining_Unit_Name (Specification (Subp_Decl));
 
-            All_Cases := Expression (Arg1);
+            --  The pragma is analyzed at the end of the declarative part which
+            --  contains the related subprogram. Reset the analyzed flag.
 
-            --  Multiple contract cases appear in aggregate form
+            Set_Analyzed (N, False);
 
-            if Nkind (All_Cases) = N_Aggregate then
-               if No (Component_Associations (All_Cases)) then
-                  Error_Pragma ("wrong syntax for pragma %");
+            --  When the aspect/pragma appears on a subprogram body, perform
+            --  the full analysis now.
 
-               --  Individual contract cases appear as component associations
+            if Nkind (Subp_Decl) = N_Subprogram_Body then
+               Analyze_Contract_Cases_In_Decl_Part (N);
 
-               else
-                  Contract_Case := First (Component_Associations (All_Cases));
-                  while Present (Contract_Case) loop
-                     Analyze_Contract_Case (Contract_Case);
+            --  Chain the pragma on the contract for further processing
 
-                     Next (Contract_Case);
-                  end loop;
-               end if;
             else
-               Error_Pragma ("wrong syntax for pragma %");
+               Add_Contract_Item (N, Subp_Id);
             end if;
-
-            Chain_Contract_Cases (Subp_Id);
          end Contract_Cases;
 
          ----------------
@@ -18013,6 +17906,34 @@ package body Sem_Prag is
       when Pragma_Exit => null;
    end Analyze_Pragma;
 
+   ------------------------------------
+   -- Analyze_Test_Case_In_Decl_Part --
+   ------------------------------------
+
+   procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id) is
+   begin
+      --  Install formals and push subprogram spec onto scope stack so that we
+      --  can see the formals from the pragma.
+
+      Push_Scope (S);
+      Install_Formals (S);
+
+      --  Preanalyze the boolean expressions, we treat these as spec
+      --  expressions (i.e. similar to a default expression).
+
+      if Pragma_Name (N) = Name_Test_Case then
+         Preanalyze_CTC_Args
+           (N,
+            Get_Requires_From_CTC_Pragma (N),
+            Get_Ensures_From_CTC_Pragma (N));
+      end if;
+
+      --  Remove the subprogram from the scope stack now that the pre-analysis
+      --  of the expressions in the contract case or test case is done.
+
+      End_Scope;
+   end Analyze_Test_Case_In_Decl_Part;
+
    ----------------
    -- Check_Kind --
    ----------------
@@ -18136,6 +18057,75 @@ package body Sem_Prag is
                                       Name_Priority_Specific_Dispatching);
    end Delay_Config_Pragma_Analyze;
 
+   -----------------------------
+   -- Find_Related_Subprogram --
+   -----------------------------
+
+   function Find_Related_Subprogram
+     (Prag             : Node_Id;
+      Check_Duplicates : Boolean := False) return Node_Id
+   is
+      Context   : constant Node_Id := Parent (Prag);
+      Nam       : constant Name_Id := Pragma_Name (Prag);
+      Decl      : Node_Id;
+      Subp_Decl : Node_Id;
+
+   begin
+      --  The pragma is a byproduct of an aspect
+
+      if Present (Corresponding_Aspect (Prag)) then
+         Subp_Decl := Parent (Corresponding_Aspect (Prag));
+
+      --  The pragma is associated with a library-level subprogram
+
+      elsif Nkind (Context) = N_Compilation_Unit_Aux then
+         Subp_Decl := Unit (Parent (Context));
+
+      --  The pragma appears inside the declarative part of a subprogram body
+
+      elsif Nkind (Context) = N_Subprogram_Body then
+         Subp_Decl := Context;
+
+      --  The pragma appears someplace after its related subprogram. Inspect
+      --  all previous declarations for a suitable candidate.
+
+      else
+         Decl      := Prag;
+         Subp_Decl := Empty;
+         while Present (Prev (Decl)) loop
+            Decl := Prev (Decl);
+
+            if Nkind (Decl) in N_Generic_Declaration then
+               Subp_Decl := Decl;
+            else
+               Subp_Decl := Original_Node (Decl);
+            end if;
+
+            --  Skip prior pragmas
+
+            if Nkind (Subp_Decl) = N_Pragma then
+               if Check_Duplicates and then Pragma_Name (Subp_Decl) = Nam then
+                  Error_Msg_Name_1 := Nam;
+                  Error_Msg_Sloc   := Sloc (Subp_Decl);
+                  Error_Msg_N ("pragma % duplicates pragma declared #", Prag);
+               end if;
+
+            --  Skip internally generated code
+
+            elsif not Comes_From_Source (Subp_Decl) then
+               null;
+
+            --  The nearest preceding declaration is the related subprogram
+
+            else
+               exit;
+            end if;
+         end loop;
+      end if;
+
+      return Subp_Decl;
+   end Find_Related_Subprogram;
+
    -------------------------
    -- Get_Base_Subprogram --
    -------------------------
@@ -18855,7 +18845,10 @@ package body Sem_Prag is
    -- Requires_Profile_Installation --
    -----------------------------------
 
-   function Requires_Profile_Installation (Subp : Node_Id) return Boolean is
+   function Requires_Profile_Installation
+     (Prag : Node_Id;
+      Subp : Node_Id) return Boolean
+   is
    begin
       --  When aspects Depends and Global are associated with a subprogram
       --  declaration, their corresponding pragmas are analyzed at the end of
@@ -18868,12 +18861,15 @@ package body Sem_Prag is
       --  When aspects Depends and Global are associated with a subprogram body
       --  which is also a compilation unit, their corresponding pragmas appear
       --  in the Pragmas_After list. The Pragmas_After collection is analyzed
-      --  out of context and the formals must be installed in visibility.
+      --  out of context and the formals must be installed in visibility. This
+      --  does not apply when the pragma is a source construct.
 
-      elsif Nkind (Subp) = N_Subprogram_Body
-        and then Nkind (Parent (Subp)) = N_Compilation_Unit
-      then
-         return True;
+      elsif Nkind (Subp) = N_Subprogram_Body then
+         if Nkind (Parent (Subp)) = N_Compilation_Unit then
+            return Present (Corresponding_Aspect (Prag));
+         else
+            return False;
+         end if;
 
       --  In all other cases the two corresponding pragmas are analyzed in
       --  context and the formals are already visibile.
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 5bf118a3867..3b8a3bcbc89 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -38,13 +38,8 @@ package Sem_Prag is
    procedure Analyze_Pragma (N : Node_Id);
    --  Analyze procedure for pragma reference node N
 
-   procedure Analyze_CTC_In_Decl_Part (N : Node_Id; S : Entity_Id);
-   --  Special analyze routine for contract-case and test-case pragmas that
-   --  appears within a declarative part where the pragma is associated with
-   --  a subprogram specification. N is the pragma node, and S is the entity
-   --  for the related subprogram. This procedure does a preanalysis of the
-   --  expressions in the pragma as "spec expressions" (see section in Sem
-   --  "Handling of Default and Per-Object Expressions...").
+   procedure Analyze_Contract_Cases_In_Decl_Part (N : Node_Id);
+   --  Perform full analysis and expansion of delayed pragma Contract_Cases
 
    procedure Analyze_Depends_In_Decl_Part (N : Node_Id);
    --  Perform full analysis of delayed pragma Depends
@@ -60,6 +55,14 @@ package Sem_Prag is
    --  of the expressions in the pragma as "spec expressions" (see section
    --  in Sem "Handling of Default and Per-Object Expressions...").
 
+   procedure Analyze_Test_Case_In_Decl_Part (N : Node_Id; S : Entity_Id);
+   --  Special analyze routine for contract-case and test-case pragmas that
+   --  appears within a declarative part where the pragma is associated with
+   --  a subprogram specification. N is the pragma node, and S is the entity
+   --  for the related subprogram. This procedure does a preanalysis of the
+   --  expressions in the pragma as "spec expressions" (see section in Sem
+   --  "Handling of Default and Per-Object Expressions...").
+
    function Check_Kind (Nam : Name_Id) return Name_Id;
    --  This function is used in connection with pragmas Assert, Check,
    --  and assertion aspects and pragmas, to determine if Check pragmas