[Ada] Do not issue a warning on a postcondition of True or False

[Ada] Do not issue a warning on a postcondition of True or False

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 465 bytes --]

Do not issue a warning about the postcondition of a function not
mentioning its result when this postcondition is statically True or
False, as this is a specification of non-termination (for value False)
or a hint to SPARK prover for not inlining an expression function (for
value True). In any case, the warning brings no value here.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* sem_util.adb (Check_Result_And_Post_State): Exempt trivial
	post.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 3278 bytes --]

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4813,6 +4813,9 @@ package body Sem_Util is
       --  and post-state. Prag is a [refined] postcondition or a contract-cases
       --  pragma. Result_Seen is set when the pragma mentions attribute 'Result
 
+      function Is_Trivial_Boolean (N : Node_Id) return Boolean;
+      --  Determine whether source node N denotes "True" or "False"
+
       -------------------------------------------
       -- Check_Result_And_Post_State_In_Pragma --
       -------------------------------------------
@@ -4836,9 +4839,6 @@ package body Sem_Util is
          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.
@@ -5089,20 +5089,6 @@ package body Sem_Util is
             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 --
          -------------------------
@@ -5202,6 +5188,20 @@ package body Sem_Util is
          end if;
       end Check_Result_And_Post_State_In_Pragma;
 
+      ------------------------
+      -- 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;
+
       --  Local variables
 
       Items        : constant Node_Id := Contract (Subp_Id);
@@ -5305,10 +5305,14 @@ package body Sem_Util is
       elsif Present (Case_Prag) and then not Seen_In_Case then
          Error_Msg_N ("contract cases do not mention result?.t?", Case_Prag);
 
-      --  The function has postconditions only and they do not mention
-      --  attribute 'Result.
+      --  The function has non-trivial postconditions only and they do not
+      --  mention attribute 'Result.
 
-      elsif Present (Post_Prag) and then not Seen_In_Post then
+      elsif Present (Post_Prag)
+        and then not Seen_In_Post
+        and then not Is_Trivial_Boolean
+          (Get_Pragma_Arg (First (Pragma_Argument_Associations (Post_Prag))))
+      then
          Error_Msg_N
            ("postcondition does not mention function result?.t?", Post_Prag);
       end if;