From patchwork Mon Mar 19 16:31:36 2012 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 147576 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) by ozlabs.org (Postfix) with SMTP id A07F1B6FC9 for ; Tue, 20 Mar 2012 03:32:22 +1100 (EST) Comment: DKIM? See http://www.dkim.org DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d=gcc.gnu.org; s=default; x=1332779542; h=Comment: DomainKey-Signature:Received:Received:Received:Received:Received: Received:Received:Date:From:To:Cc:Subject:Message-ID: MIME-Version:Content-Type:Content-Disposition:User-Agent: Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive: List-Post:List-Help:Sender:Delivered-To; bh=+mRtwf9ibLHI+nvJMOEs cgosOI0=; b=mjXs/AzihybM0zWMvjCUmJOiN7gZxV+JunbmT1jkW1mCpI7iqr6X CHovuFaJHjyXJfVmdkrrX7ah5cTjX6FwpWCrKS5xbngSfzBvVWoPUOv+JqePpOxD lCTrFU7fQ2j3TSRTjIWfi1826OKbOlnWtCzp+8ZTVVbTTzDlHwbqC3g= Comment: DomainKeys? See http://antispam.yahoo.com/domainkeys DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=default; d=gcc.gnu.org; h=Received:Received:X-SWARE-Spam-Status:X-Spam-Check-By:Received:Received:Received:Received:Received:Date:From:To:Cc:Subject:Message-ID:MIME-Version:Content-Type:Content-Disposition:User-Agent:Mailing-List:Precedence:List-Id:List-Unsubscribe:List-Archive:List-Post:List-Help:Sender:Delivered-To; b=AgPIPm7GdQiAJMp7T5otnpdExSzfwp+3bcgAorJp7OkBDkLd9JxweRDGGDSobx +6ssgvouhBxp8bBdVIlx+TnufbzLCxk90wDL87BrLD86CT6PcyWdXZIlkqCjQNg9 Y4xo2Ua6HtvjVT9yYDKUdA9QxS3j2xBGpURQ9obnTRBr0=; Received: (qmail 26062 invoked by alias); 19 Mar 2012 16:32:19 -0000 Received: (qmail 26050 invoked by uid 22791); 19 Mar 2012 16:32:17 -0000 X-SWARE-Spam-Status: No, hits=-1.8 required=5.0 tests=AWL,BAYES_00 X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Mon, 19 Mar 2012 16:31:38 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 9A3171C67A9; Mon, 19 Mar 2012 12:31:36 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id iflslE+92Myi; Mon, 19 Mar 2012 12:31:36 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 750E81C679F; Mon, 19 Mar 2012 12:31:36 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 73EA93FEE8; Mon, 19 Mar 2012 12:31:36 -0400 (EDT) Date: Mon, 19 Mar 2012 12:31:36 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Remove spurious warning with -gnatw.t on trivial postconditions Message-ID: <20120319163136.GA19507@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org It may be useful to have trivial postconditions of "True" or "False" on some subprograms. The first is essentially a confirming postcondition, while the second indicates that a procedure will not return (if postconditions are checked). Do not emit warnings on such postconditions. Similarly for Ensures components of contract-cases. GNAT does not issue warnings on the following code: $ gcc -c -gnatc -gnat12 -gnatw.t p.ads 1. package P is 2. function Func return Boolean with 3. Post => True, 4. Contract_Case => (Name => "all", 5. Mode => Nominal, 6. Ensures => True); 7. procedure Proc with 8. Post => False, 9. Contract_Case => (Name => "all", 10. Mode => Nominal, 11. Ensures => False); 12. end P; Tested on x86_64-pc-linux-gnu, committed on trunk 2012-03-19 Yannick Moy * sem_ch6.adb (Check_Subprogram_Contract): Do not emit warnings on trivially True or False postconditions and Ensures components of contract-cases. Index: sem_ch6.adb =================================================================== --- sem_ch6.adb (revision 185520) +++ sem_ch6.adb (working copy) @@ -6927,23 +6927,29 @@ -- Inherited_Subprograms (Spec_Id); -- -- List of subprograms inherited by this subprogram + -- We ignore postconditions "True" or "False" and contract-cases which + -- have similar Ensures components, which we call "trivial", when + -- issuing warnings, since these postconditions and contract-cases + -- purposedly ignore the post-state. + Last_Postcondition : Node_Id := Empty; - -- Last postcondition on the subprogram, or else Empty if either no - -- postcondition or only inherited postconditions. + -- Last non-trivial postcondition on the subprogram, or else Empty if + -- either no non-trivial postcondition or only inherited postconditions. Last_Contract_Case : Node_Id := Empty; - -- Last contract-case on the subprogram, or else Empty + -- Last non-trivial contract-case on the subprogram, or else Empty Attribute_Result_Mentioned : Boolean := False; - -- Whether attribute 'Result is mentioned in a postcondition + -- Whether attribute 'Result is mentioned in a non-trivial postcondition + -- or contract-case. No_Warning_On_Some_Postcondition : Boolean := False; - -- Whether there exists a postcondition or a contract-case without a - -- corresponding warning. + -- Whether there exists a non-trivial postcondition or contract-case + -- without a corresponding warning. Post_State_Mentioned : Boolean := False; - -- Whether some expression mentioned in a postcondition can have a - -- different value in the post-state than in the pre-state. + -- Whether some expression mentioned in a postcondition or contract-case + -- can have a different value in the post-state than in the pre-state. function Check_Attr_Result (N : Node_Id) return Traverse_Result; -- Check if N is a reference to the attribute 'Result, and if so set @@ -6956,6 +6962,9 @@ -- reference to attribute 'Old, in order to ignore its prefix, which -- is precisely evaluated in the pre-state. Otherwise return OK. + function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean; + -- Return whether node N is trivially "True" or "False" + procedure Process_Contract_Cases (Spec : Node_Id); -- This processes the Spec_CTC_List from Spec, processing any contract -- case from the list. The caller has checked that Spec_CTC_List is @@ -7046,13 +7055,26 @@ end if; end Check_Post_State; + -------------------------------- + -- Is_Trivial_Post_Or_Ensures -- + -------------------------------- + + function Is_Trivial_Post_Or_Ensures (N : Node_Id) return Boolean is + begin + return Is_Entity_Name (N) + and then (Entity (N) = Standard_True + or else + Entity (N) = Standard_False); + end Is_Trivial_Post_Or_Ensures; + ---------------------------- -- Process_Contract_Cases -- ---------------------------- procedure Process_Contract_Cases (Spec : Node_Id) is - Prag : Node_Id; - Arg : Node_Id; + Prag : Node_Id; + Arg : Node_Id; + Ignored : Traverse_Final_Result; pragma Unreferenced (Ignored); @@ -7063,8 +7085,12 @@ Arg := Get_Ensures_From_CTC_Pragma (Prag); - if Pragma_Name (Prag) = Name_Contract_Case then + -- Ignore trivial contract-case when Ensures component is "True" + -- or "False". + if Pragma_Name (Prag) = Name_Contract_Case + and then not Is_Trivial_Post_Or_Ensures (Expression (Arg)) + then -- Since contract-cases are listed in reverse order, the first -- contract-case in the list is the last in the source. @@ -7088,8 +7114,8 @@ if Post_State_Mentioned then No_Warning_On_Some_Postcondition := True; else - Error_Msg_N ("?`Ensures` component refers only to pre-state", - Prag); + Error_Msg_N + ("?`Ensures` component refers only to pre-state", Prag); end if; end if; @@ -7116,8 +7142,11 @@ loop Arg := First (Pragma_Argument_Associations (Prag)); - if Pragma_Name (Prag) = Name_Postcondition then + -- Ignore trivial postcondition of "True" or "False" + if Pragma_Name (Prag) = Name_Postcondition + and then not Is_Trivial_Post_Or_Ensures (Expression (Arg)) + then -- Since pre- and post-conditions are listed in reverse order, -- the first postcondition in the list is last in the source.