2014-01-20 Hristian Kirtchev <kirtchev@adacore.com>

	* sem_attr.adb (Analyze_Attribute): Attributes 'Old and 'Result
	can now apply to a refined postcondition.
	* sem_ch6.adb (Analyze_Subprogram_Contract): Remove local
	variable Result_Seen. Add variables Case_Prag, Post_Prag,
	Seen_In_Case and Seen_In_Post. Update the mechanism that detects
	whether postconditions and/or constract-cases mention attribute
	'Result and introduce a post-state when applied to functions.
	(Check_Result_And_Post_State): Removed.
	* sem_prag.adb (Analyze_Pragma): Add local variable
	Result_Seen. Verify that the expression of pragma Refined_Post
	mentions attribute 'Result and introduces a post-state.
	* sem_util.ads, sem_util.adb (Check_Result_And_Post_State): New routine.

2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch7.adb (Is_Subprogram_Call): New routine.
	(Process_Transient_Objects): Make variable Must_Hook global with
	respect to all locally declared subprograms. Search the context
	for at least one subprogram call.
	(Requires_Hooking): Removed.

2014-01-20  Claire Dross  <dross@adacore.com>

	* a-cfdlli.ads a-cfhama.ads a-cfhase.ads a-cforma.ads
	* a-cforse.ads a-cofove.ads: Add pragma Annotate (GNATprove,
	External_Axiomatization);



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@206819 138bc75d-0d04-0410-961f-82ee72b054a4

13 files changed, 394 insertions, 295 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 442465517c5..d1e8fcfe0ea 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,32 @@
+2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_attr.adb (Analyze_Attribute): Attributes 'Old and 'Result
+	can now apply to a refined postcondition.
+	* sem_ch6.adb (Analyze_Subprogram_Contract): Remove local
+	variable Result_Seen. Add variables Case_Prag, Post_Prag,
+	Seen_In_Case and Seen_In_Post. Update the mechanism that detects
+	whether postconditions and/or constract-cases mention attribute
+	'Result and introduce a post-state when applied to functions.
+	(Check_Result_And_Post_State): Removed.
+	* sem_prag.adb (Analyze_Pragma): Add local variable
+	Result_Seen. Verify that the expression of pragma Refined_Post
+	mentions attribute 'Result and introduces a post-state.
+	* sem_util.ads, sem_util.adb (Check_Result_And_Post_State): New routine.
+
+2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_ch7.adb (Is_Subprogram_Call): New routine.
+	(Process_Transient_Objects): Make variable Must_Hook global with
+	respect to all locally declared subprograms. Search the context
+	for at least one subprogram call.
+	(Requires_Hooking): Removed.
+
+2014-01-20  Claire Dross  <dross@adacore.com>
+
+	* a-cfdlli.ads a-cfhama.ads a-cfhase.ads a-cforma.ads
+	* a-cforse.ads a-cofove.ads: Add pragma Annotate (GNATprove,
+	External_Axiomatization);
+
 2014-01-20  Robert Dewar  <dewar@adacore.com>
 
 	* sem_attr.adb (Analyze_Attribute, case Loop_Entry): Allow
diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads
index b15b2425e4d..660eb18e302 100644
--- a/gcc/ada/a-cfdlli.ads
+++ b/gcc/ada/a-cfdlli.ads
@@ -60,6 +60,7 @@ generic
                       return Boolean is <>;
 
 package Ada.Containers.Formal_Doubly_Linked_Lists is
+   pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
    type List (Capacity : Count_Type) is private;
diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index dbfcb82e9dc..5366655753e 100644
--- a/gcc/ada/a-cfhama.ads
+++ b/gcc/ada/a-cfhama.ads
@@ -64,6 +64,7 @@ generic
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Hashed_Maps is
+   pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private;
diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads
index c0103cbe0f4..d470e1b8a9f 100644
--- a/gcc/ada/a-cfhase.ads
+++ b/gcc/ada/a-cfhase.ads
@@ -66,6 +66,7 @@ generic
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Hashed_Sets is
+   pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private;
diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index 2ddbd90a1ab..00cd3989d52 100644
--- a/gcc/ada/a-cforma.ads
+++ b/gcc/ada/a-cforma.ads
@@ -65,6 +65,7 @@ generic
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Ordered_Maps is
+   pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
    function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads
index 1d8cdf66786..0116e8f2791 100644
--- a/gcc/ada/a-cforse.ads
+++ b/gcc/ada/a-cforse.ads
@@ -63,6 +63,7 @@ generic
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Ordered_Sets is
+   pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads
index 604ed8d356b..9ee2ea99eed 100644
--- a/gcc/ada/a-cofove.ads
+++ b/gcc/ada/a-cofove.ads
@@ -62,6 +62,7 @@ generic
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
 package Ada.Containers.Formal_Vectors is
+   pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
    subtype Extended_Index is Index_Type'Base
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index a5238585b6c..25e4ef3c624 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -4480,33 +4480,45 @@ package body Exp_Ch7 is
          Last_Object  : Node_Id;
          Related_Node : Node_Id)
       is
-         function Requires_Hooking return Boolean;
-         --  Determine whether the context requires transient variable export
-         --  to the outer finalizer. This scenario arises when the context may
-         --  raise an exception.
+         Must_Hook : Boolean := False;
+         --  Flag denoting whether the context requires transient variable
+         --  export to the outer finalizer.
 
-         ----------------------
-         -- Requires_Hooking --
-         ----------------------
+         function Is_Subprogram_Call (N : Node_Id) return Traverse_Result;
+         --  Determine whether an arbitrary node denotes a subprogram call
 
-         function Requires_Hooking return Boolean is
+         ------------------------
+         -- Is_Subprogram_Call --
+         ------------------------
+
+         function Is_Subprogram_Call (N : Node_Id) return Traverse_Result is
          begin
-            --  The context is either a procedure or function call or an object
-            --  declaration initialized by a function call. Note that in the
-            --  latter case, a function call that returns on the secondary
-            --  stack is usually rewritten into something else. Its proper
-            --  detection requires examination of the original initialization
-            --  expression.
-
-            return Nkind (N) in N_Subprogram_Call
-              or else (Nkind (N) = N_Object_Declaration
-                         and then Nkind (Original_Node (Expression (N))) =
-                                    N_Function_Call);
-         end Requires_Hooking;
+            --  A regular procedure or function call
+
+            if Nkind (N) in N_Subprogram_Call then
+               Must_Hook := True;
+               return Abandon;
+
+            --  Detect a call to a function that returns on the secondary stack
+
+            elsif Nkind (N) = N_Object_Declaration
+              and then Nkind (Original_Node (Expression (N))) = N_Function_Call
+            then
+               Must_Hook := True;
+               return Abandon;
+
+            --  Keep searching
+
+            else
+               return OK;
+            end if;
+         end Is_Subprogram_Call;
+
+         procedure Detect_Subprogram_Call is
+           new Traverse_Proc (Is_Subprogram_Call);
 
          --  Local variables
 
-         Must_Hook : constant Boolean := Requires_Hooking;
          Built     : Boolean := False;
          Desig_Typ : Entity_Id;
          Fin_Block : Node_Id;
@@ -4525,6 +4537,12 @@ package body Exp_Ch7 is
       --  Start of processing for Process_Transient_Objects
 
       begin
+         --  Search the context for at least one subprogram call. If found, the
+         --  machinery exports all transient objects to the enclosing finalizer
+         --  due to the possibility of abnormal call termination.
+
+         Detect_Subprogram_Call (N);
+
          --  Examine all objects in the list First_Object .. Last_Object
 
          Stmt := First_Object;
diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb
index dbfbcd98e74..934faebbf9e 100644
--- a/gcc/ada/sem_attr.adb
+++ b/gcc/ada/sem_attr.adb
@@ -4357,52 +4357,68 @@ package body Sem_Attr is
             if Nkind (Prag) = N_Aspect_Specification then
                null;
 
+            --  We must have a pragma
+
             elsif Nkind (Prag) /= N_Pragma then
                Error_Attr ("% attribute can only appear in postcondition", P);
 
-            elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
-               declare
-                  Arg_Ens : constant Node_Id :=
-                              Get_Ensures_From_CTC_Pragma (Prag);
-                  Arg     : Node_Id;
+            --  Processing depends on which pragma we have
 
-               begin
-                  Arg := N;
-                  while Arg /= Prag and then Arg /= Arg_Ens loop
-                     Arg := Parent (Arg);
-                  end loop;
+            else
+               case Get_Pragma_Id (Prag) is
+                  when Pragma_Test_Case =>
+                     declare
+                        Arg_Ens : constant Node_Id :=
+                                    Get_Ensures_From_CTC_Pragma (Prag);
+                        Arg     : Node_Id;
 
-                  if Arg /= Arg_Ens then
-                     Error_Attr ("% attribute misplaced inside test case", P);
-                  end if;
-               end;
+                     begin
+                        Arg := N;
+                        while Arg /= Prag and then Arg /= Arg_Ens loop
+                           Arg := Parent (Arg);
+                        end loop;
+
+                        if Arg /= Arg_Ens then
+                           Error_Attr
+                             ("% attribute misplaced inside test case", P);
+                        end if;
+                     end;
 
-            elsif Get_Pragma_Id (Prag) = Pragma_Contract_Cases then
-               declare
-                  Aggr : constant Node_Id :=
-                    Expression (First (Pragma_Argument_Associations (Prag)));
-                  Arg  : Node_Id;
+                  when Pragma_Contract_Cases =>
+                     declare
+                        Aggr : constant Node_Id :=
+                          Expression
+                            (First (Pragma_Argument_Associations (Prag)));
+                        Arg  : Node_Id;
 
-               begin
-                  Arg := N;
-                  while Arg /= Prag and then Parent (Parent (Arg)) /= Aggr loop
-                     Arg := Parent (Arg);
-                  end loop;
+                     begin
+                        Arg := N;
+                        while Arg /= Prag
+                          and then Parent (Parent (Arg)) /= Aggr
+                        loop
+                           Arg := Parent (Arg);
+                        end loop;
+
+                        --  At this point, Parent (Arg) should be a component
+                        --  association. Attribute Result is only allowed in
+                        --  the expression part of this association.
+
+                        if Nkind (Parent (Arg)) /= N_Component_Association
+                          or else Arg /= Expression (Parent (Arg))
+                        then
+                           Error_Attr
+                             ("% attribute misplaced inside contract cases",
+                              P);
+                        end if;
+                     end;
 
-                  --  At this point, Parent (Arg) should be a component
-                  --  association. Attribute Result is only allowed in
-                  --  the expression part of this association.
+                  when Pragma_Postcondition | Pragma_Refined_Post =>
+                     null;
 
-                  if Nkind (Parent (Arg)) /= N_Component_Association
-                    or else Arg /= Expression (Parent (Arg))
-                  then
+                  when others =>
                      Error_Attr
-                       ("% attribute misplaced inside contract cases", P);
-                  end if;
-               end;
-
-            elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then
-               Error_Attr ("% attribute can only appear in postcondition", P);
+                       ("% attribute can only appear in postcondition", P);
+               end case;
             end if;
 
          --  Check the legality of attribute 'Old when it appears inside pragma
@@ -4796,56 +4812,72 @@ package body Sem_Attr is
             if Nkind (Prag) = N_Aspect_Specification then
                null;
 
+            --  Must have a pragma
+
             elsif Nkind (Prag) /= N_Pragma then
                Error_Attr
                  ("% attribute can only appear in postcondition of function",
                   P);
 
-            elsif Get_Pragma_Id (Prag) = Pragma_Test_Case then
-               declare
-                  Arg_Ens : constant Node_Id :=
-                              Get_Ensures_From_CTC_Pragma (Prag);
-                  Arg     : Node_Id;
+            --  Processing depends on which pragma we have
 
-               begin
-                  Arg := N;
-                  while Arg /= Prag and then Arg /= Arg_Ens loop
-                     Arg := Parent (Arg);
-                  end loop;
+            else
+               case Get_Pragma_Id (Prag) is
 
-                  if Arg /= Arg_Ens then
-                     Error_Attr ("% attribute misplaced inside test case", P);
-                  end if;
-               end;
+                  when Pragma_Test_Case =>
+                     declare
+                        Arg_Ens : constant Node_Id :=
+                                    Get_Ensures_From_CTC_Pragma (Prag);
+                        Arg     : Node_Id;
 
-            elsif Get_Pragma_Id (Prag) = Pragma_Contract_Cases then
-               declare
-                  Aggr : constant Node_Id :=
-                    Expression (First (Pragma_Argument_Associations (Prag)));
-                  Arg  : Node_Id;
+                     begin
+                        Arg := N;
+                        while Arg /= Prag and then Arg /= Arg_Ens loop
+                           Arg := Parent (Arg);
+                        end loop;
+
+                        if Arg /= Arg_Ens then
+                           Error_Attr
+                             ("% attribute misplaced inside test case", P);
+                        end if;
+                     end;
 
-               begin
-                  Arg := N;
-                  while Arg /= Prag and then Parent (Parent (Arg)) /= Aggr loop
-                     Arg := Parent (Arg);
-                  end loop;
+                  when Pragma_Contract_Cases =>
+                     declare
+                        Aggr : constant Node_Id :=
+                          Expression (First
+                                        (Pragma_Argument_Associations (Prag)));
+                        Arg  : Node_Id;
 
-                  --  At this point, Parent (Arg) should be a component
-                  --  association. Attribute Result is only allowed in
-                  --  the expression part of this association.
+                     begin
+                        Arg := N;
+                        while Arg /= Prag
+                          and then Parent (Parent (Arg)) /= Aggr
+                        loop
+                           Arg := Parent (Arg);
+                        end loop;
+
+                        --  At this point, Parent (Arg) should be a component
+                        --  association. Attribute Result is only allowed in
+                        --  the expression part of this association.
+
+                        if Nkind (Parent (Arg)) /= N_Component_Association
+                          or else Arg /= Expression (Parent (Arg))
+                        then
+                           Error_Attr
+                             ("% attribute misplaced inside contract cases",
+                              P);
+                        end if;
+                     end;
 
-                  if Nkind (Parent (Arg)) /= N_Component_Association
-                    or else Arg /= Expression (Parent (Arg))
-                  then
-                     Error_Attr
-                       ("% attribute misplaced inside contract cases", P);
-                  end if;
-               end;
+                  when Pragma_Postcondition | Pragma_Refined_Post =>
+                     null;
 
-            elsif Get_Pragma_Id (Prag) /= Pragma_Postcondition then
-               Error_Attr
-                 ("% attribute can only appear in postcondition of function",
-                  P);
+                     when others =>
+                        Error_Attr
+                          ("% attribute can only appear in postcondition "
+                           & "of function", P);
+               end case;
             end if;
 
             --  The attribute reference is a primary. If expressions follow,
@@ -4866,8 +4898,8 @@ package body Sem_Attr is
 
             Set_Etype (N, Etype (CS));
 
-            --  If several functions with that name are visible,
-            --  the intended one is the current scope.
+            --  If several functions with that name are visible, the intended
+            --  one is the current scope.
 
             if Is_Overloaded (P) then
                Set_Entity (P, CS);
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index a7cadbd97df..52a81af781b 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3420,190 +3420,15 @@ package body Sem_Ch6 is
    ---------------------------------
 
    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);
-      Depends     : Node_Id := Empty;
-      Error_CCase : Node_Id := Empty;
-      Error_Post  : Node_Id := Empty;
-      Global      : Node_Id := Empty;
-      Nam         : Name_Id;
-      Prag        : Node_Id;
-
-   --  Start of processing for Analyze_Subprogram_Contract
+      Items        : constant Node_Id := Contract (Subp);
+      Case_Prag    : Node_Id := Empty;
+      Depends      : Node_Id := Empty;
+      Global       : Node_Id := Empty;
+      Nam          : Name_Id;
+      Post_Prag    : Node_Id := Empty;
+      Prag         : Node_Id;
+      Seen_In_Case : Boolean := False;
+      Seen_In_Post : Boolean := False;
 
    begin
       if Present (Items) then
@@ -3620,7 +3445,8 @@ package body Sem_Ch6 is
             if Warn_On_Suspicious_Contract
               and then Pragma_Name (Prag) = Name_Postcondition
             then
-               Check_Result_And_Post_State (Prag, Error_Post);
+               Post_Prag := Prag;
+               Check_Result_And_Post_State (Prag, Seen_In_Post);
             end if;
 
             Prag := Next_Pragma (Prag);
@@ -3642,7 +3468,8 @@ package body Sem_Ch6 is
                if Warn_On_Suspicious_Contract
                  and then not Error_Posted (Prag)
                then
-                  Check_Result_And_Post_State (Prag, Error_CCase);
+                  Case_Prag := Prag;
+                  Check_Result_And_Post_State (Prag, Seen_In_Case);
                end if;
 
             else
@@ -3683,26 +3510,28 @@ package body Sem_Ch6 is
          end if;
       end if;
 
-      --  Emit an error when none of the postconditions or contract-cases
+      --  Emit an error when neither the postconditions nor the 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
+         if Present (Case_Prag)
+           and then not Seen_In_Case
+           and then Present (Post_Prag)
+           and then not Seen_In_Post
+         then
             Error_Msg_N
               ("neither function postcondition nor contract cases mention "
-               & "result?T?", Error_Post);
+               & "result?T?", Post_Prag);
 
-         elsif Present (Error_Post) then
+         elsif Present (Case_Prag) and then not Seen_In_Case then
             Error_Msg_N
-              ("function postcondition does not mention result?T?",
-               Error_Post);
+              ("contract cases do not mention result?T?", Case_Prag);
 
-         elsif Present (Error_CCase) then
+         elsif Present (Post_Prag) and then not Seen_In_Post then
             Error_Msg_N
-              ("contract cases do not mention result?T?", Error_CCase);
+              ("function postcondition does not mention result?T?", Post_Prag);
          end if;
       end if;
    end Analyze_Subprogram_Contract;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index c7488550677..ebb68431477 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -17331,9 +17331,10 @@ package body Sem_Prag is
          --  pragma Refined_Post (boolean_EXPRESSION);
 
          when Pragma_Refined_Post => Refined_Post : declare
-            Body_Id : Entity_Id;
-            Legal   : Boolean;
-            Spec_Id : Entity_Id;
+            Body_Id     : Entity_Id;
+            Legal       : Boolean;
+            Result_Seen : Boolean := False;
+            Spec_Id     : Entity_Id;
 
          begin
             Analyze_Refined_Pragma (Spec_Id, Body_Id, Legal);
@@ -17342,6 +17343,20 @@ package body Sem_Prag is
 
             if Legal then
                Analyze_Pre_Post_Condition_In_Decl_Part (N, Spec_Id);
+
+               --  Verify that the refined postcondition mentions attribute
+               --  'Result and its expression introduces a post-state.
+
+               if Warn_On_Suspicious_Contract
+                 and then Ekind_In (Spec_Id, E_Function, E_Generic_Function)
+               then
+                  Check_Result_And_Post_State (N, Result_Seen);
+
+                  if not Result_Seen then
+                     Error_Pragma
+                       ("pragma % does not mention function result?T?");
+                  end if;
+               end if;
             end if;
          end Refined_Post;
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 7a1920c6c0a..476fe7da7c9 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -2396,6 +2396,168 @@ package body Sem_Util is
       end loop;
    end Check_Potentially_Blocking_Operation;
 
+   ---------------------------------
+   -- Check_Result_And_Post_State --
+   ---------------------------------
+
+   procedure Check_Result_And_Post_State
+     (Prag        : Node_Id;
+      Result_Seen : in out Boolean)
+   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);
+
+               elsif Pragma_Name (Prag) = Name_Refined_Post then
+                  Error_Msg_N
+                    ("refined postcondition refers only to pre-state?T?",
+                     Prag);
+
+               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 Is_Attribute_Result (N) 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 :=
+                Get_Pragma_Arg (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
+      --  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_In (Nam, Name_Postcondition, Name_Refined_Post));
+         Check_Expression (Expr);
+      end if;
+   end Check_Result_And_Post_State;
+
    ------------------------------
    -- Check_Unprotected_Access --
    ------------------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 8227ee2735b..4bd32b495df 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -260,6 +260,14 @@ package Sem_Util is
    --  N is one of the statement forms that is a potentially blocking
    --  operation. If it appears within a protected action, emit warning.
 
+   procedure Check_Result_And_Post_State
+     (Prag        : Node_Id;
+      Result_Seen : in out Boolean);
+   --  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 [refined] postcondition or a contract-cases
+   --  pragma. Result_Seen is set when the pragma mentions attribute 'Result.
+
    procedure Check_Unprotected_Access
      (Context : Node_Id;
       Expr    : Node_Id);