From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wm1-x32f.google.com (mail-wm1-x32f.google.com [IPv6:2a00:1450:4864:20::32f]) by sourceware.org (Postfix) with ESMTPS id 76D57383D807 for ; Thu, 12 May 2022 12:40:10 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 76D57383D807 Received: by mail-wm1-x32f.google.com with SMTP id bg25so2944958wmb.4 for ; Thu, 12 May 2022 05:40:10 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=TBARLhuR3zsNoweMm0BahoXpSKTB1apsQpHZoTNF6/s=; b=2/sp5gFwEIhcQ8iQ/9nuZavb296DnCgRuRJNeZiADqMCoVW++fXib4xzOiCd4+kuJO QCFmKpLdKcw8jaSk4UfwvoOkP0YDus2awdYg9cUxyA8x8UV5t1p9lNpW+nUv3aeVJsIl SDltNkfnbPdioLAl7JtzON5uRV26YXgHLCLVzEUIuE3QQwfKy+EIO+7x4Hux58PNV4t1 lu6HGYqehCgS61Z4m1VJHz3HXSDGQz+B7NcAbg3Awo/3GOqdQJ3MkJgCb1Ykq7zoWvzq ppFJZFLNj93Al8KM2J+tV2uc5TCrDHshhGxuRmhQwQa8kuXnVyO5gsAE/HKDxrIMUxZx c3EQ== X-Gm-Message-State: AOAM531IUKpptqZTWirTQ9IqfYrg29Ag1+OCBBT0b0UZRMkkXjc0OGuZ 9rBFK/sb7JcZNs4i0VCViQD61CHR/V9EmQ== X-Google-Smtp-Source: ABdhPJx87QHE+U4BPsJzdnDCqVGCSmrCNZgAEXHAQIdlV3FjFzNMxPqh6x4LRoCpqqovbHmjQmD4Mw== X-Received: by 2002:a05:600c:1d10:b0:394:737f:e36 with SMTP id l16-20020a05600c1d1000b00394737f0e36mr10124500wms.202.1652359209222; Thu, 12 May 2022 05:40:09 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id v9-20020adff689000000b0020c5253d902sm3975839wrp.78.2022.05.12.05.40.08 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 12 May 2022 05:40:08 -0700 (PDT) Date: Thu, 12 May 2022 12:40:08 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Do not issue a warning on a postcondition of True or False Message-ID: <20220512124008.GA781034@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="y0ulUmNC+osPPQO6" Content-Disposition: inline X-Spam-Status: No, score=-12.8 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 12 May 2022 12:40:12 -0000 --y0ulUmNC+osPPQO6 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline 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. --y0ulUmNC+osPPQO6 Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" 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; --y0ulUmNC+osPPQO6--