From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id 0BEC93858D1E; Tue, 20 Jun 2023 07:47:13 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 0BEC93858D1E DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1687247233; bh=nWL4m4nnTRUtCji9Veu2JmK0evFF5JYLwhJS/IMbNVg=; h=From:To:Subject:Date:From; b=K4CCuPgLq0vgbX5uefJcHkjdZuFh21L3nlGuWfAhHIX14rwiH8ORLejZV2aiDeF6f 1tiuJZp8SQBEBlQtjHnCov1+L37tkLnDZtSwyDVPRCbiPy1X2ER82tchj7N10qkkO9 6JL8xPBjbVILgfwZ/J5MmMtB7La5Pr2WyZnLrxJQ= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r14-1977] ada: Do not issue warning on postcondition in some cases X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: f1c15fe3f054d453f94e1412ec5bcb2c1e7205e8 X-Git-Newrev: 8912b95779dd233fb3a8c8b4dda033ed7b50be31 Message-Id: <20230620074713.0BEC93858D1E@sourceware.org> Date: Tue, 20 Jun 2023 07:47:13 +0000 (GMT) List-Id: https://gcc.gnu.org/g:8912b95779dd233fb3a8c8b4dda033ed7b50be31 commit r14-1977-g8912b95779dd233fb3a8c8b4dda033ed7b50be31 Author: Yannick Moy 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