[gcc r14-1977] ada: Do not issue warning on postcondition in some cases

[gcc r14-1977] ada: Do not issue warning on postcondition in some cases

[Marc Poulhi?s]

https://gcc.gnu.org/g:8912b95779dd233fb3a8c8b4dda033ed7b50be31

commit r14-1977-g8912b95779dd233fb3a8c8b4dda033ed7b50be31
Author: Yannick Moy <moy@adacore.com>
Date:   Thu Jun 8 09:12:25 2023 +0000

    ada: Do not issue warning on postcondition in some cases
    
    Warning on suspicious postcondition is not relevant if contract
    Exceptional_Cases is present, or if contract Always_Terminates is
    present with a non-statically True value, as in those cases the
    postcondition can be used to indicate constraints on those pre-state
    for which the subprogram might terminate normally.
    
    gcc/ada/
    
            * sem_util.adb (Check_Result_And_Post_State): Do not warn in cases
            where the warning could be spurious.

Diff:
---
 gcc/ada/sem_util.adb | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 3a64047d45c..1729a2addd8 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -4566,6 +4566,38 @@ package body Sem_Util is
 
       elsif No (Items) then
          return;
+
+      --  If the subprogram has a contract Exceptional_Cases, it is often
+      --  useful to refer only to the pre-state in the postcondition, to
+      --  indicate when the subprogram might terminate normally.
+
+      elsif Present (Get_Pragma (Subp_Id, Pragma_Exceptional_Cases)) then
+         return;
+
+      --  Same if the subprogram has a contract Always_Terminates => Cond,
+      --  where Cond is not syntactically True.
+
+      else
+         declare
+            Prag : constant Node_Id :=
+              Get_Pragma (Subp_Id, Pragma_Always_Terminates);
+         begin
+            if Present (Prag)
+              and then Present (Pragma_Argument_Associations (Prag))
+            then
+               declare
+                  Cond : constant Node_Id :=
+                    Get_Pragma_Arg
+                      (First (Pragma_Argument_Associations (Prag)));
+               begin
+                  if not Compile_Time_Known_Value (Cond)
+                    or else not Is_True (Expr_Value (Cond))
+                  then
+                     return;
+                  end if;
+               end;
+            end if;
+         end;
       end if;
 
       --  Examine all postconditions for attribute 'Result and a post-state