From: Yannick Moy <moy@adacore.com>
Date: Thu, 8 Jun 2023 09:12:25 +0000 (+0000)
Subject: ada: Do not issue warning on postcondition in some cases
X-Git-Tag: basepoints/gcc-15~8162
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=8912b95779dd233fb3a8c8b4dda033ed7b50be31;p=thirdparty%2Fgcc.git

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 --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 3a64047d45c1..1729a2addd86 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