From patchwork Thu Apr 25 10:29:13 2013 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 239469 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]) (using TLSv1 with cipher DHE-RSA-AES256-SHA (256/256 bits)) (Client CN "localhost", Issuer "www.qmailtoaster.com" (not verified)) by ozlabs.org (Postfix) with ESMTPS id DE3D62C00F5 for ; Thu, 25 Apr 2013 20:29:31 +1000 (EST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=hUWPs1Vvqh2GPx9UI6nTcMTYpS9Y70Wlp8S12YA1ApIM75YVQ2 qcFIBtxuNrNTG2TsG6MCeyXatpDP6nrNLfupc1Cr/h3NaiOOlaAZGEHneJW/Zkr1 0cXpfhd7bUWSsk0vIvef4XWL3c8F0ve9DxHllPayvYkrQfPWscfrBj8dk= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=r3S0Evodez94+uu+ia5eQc/Rojw=; b=FGyUIKHlmxOPAYL6GoB8 XupBSMjbHOdWMMa5ek0de0fc8LbpBlCU1hPFH2DJP8Op59eu4iiaKdPIWnEVqzei BA4T/qzlxtYoz+dHc3zJYGarm/Zr+ScS1h3OSGgitQoKGG4LfX7HauROarsjGgUR c7dIpVXclXYeAzUbLzElx8w= Received: (qmail 25282 invoked by alias); 25 Apr 2013 10:29:16 -0000 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 Received: (qmail 25246 invoked by uid 89); 25 Apr 2013 10:29:15 -0000 X-Spam-SWARE-Status: No, score=-1.8 required=5.0 tests=AWL, BAYES_00, RCVD_IN_HOSTKARMA_NO autolearn=ham version=3.3.1 Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.84/v0.84-167-ge50287c) with ESMTP; Thu, 25 Apr 2013 10:29:14 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 264EC2E890; Thu, 25 Apr 2013 06:29:13 -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 g0k0vPuag4TO; Thu, 25 Apr 2013 06:29:13 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 0E2002E7DC; Thu, 25 Apr 2013 06:29:13 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 067C13FF09; Thu, 25 Apr 2013 06:29:13 -0400 (EDT) Date: Thu, 25 Apr 2013 06:29:13 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Warning on suspicious existential quantifier Message-ID: <20130425102913.GA10737@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) X-Virus-Found: No This patch adds a check in the analysis of quantified expressions to detect a suspicious use of quantifier "some" when "all" was meant. ------------ -- Source -- ------------ -- semantics.ads package Semantics is function Error_1 (X : Integer) return Boolean with Post => (for some Y in Integer => (if Y > 5 then Error_1 (Y))); function Error_2 (X : Integer) return Boolean with Post => (for some Y in Integer => (if Y > 5 then Error_2 (Y) else True)); function OK_1 (X : Integer) return Boolean with Post => (for some Y in Integer => (if Y > 5 then OK_1 (Y) else not OK_1 (Y))); function OK_2 (X : Integer) return Boolean with Post => (for some Y in Integer => (if Y > 5 then OK_2 (Y) elsif Y = 5 then not OK_2 (Y))); function Error_3 (X : Integer) return Boolean with Post => (for some X in Integer => (for some Y in Integer => (if X > 5 then Error_3 (Y)))); function OK_3 (X : Integer) return Boolean with Post => (for all Y in Integer => (if Y > 5 then OK_3 (Y))); function OK_4 (X : Integer) return Boolean with Post => (for some Y in Integer => (OK_4 (Y))); end Semantics; ---------------------------- -- Compilation and output -- ---------------------------- $ gcc -c -gnat12 -gnatd.V semantics.ads semantics.ads:4:06: warning: function postcondition does not mention result semantics.ads:4:15: warning: suspicious expression semantics.ads:4:15: warning: did you mean (for all X => (if P then Q)) semantics.ads:4:15: warning: or (for some X => P and then Q) instead? semantics.ads:8:06: warning: function postcondition does not mention result semantics.ads:8:15: warning: suspicious expression semantics.ads:8:15: warning: did you mean (for all X => (if P then Q)) semantics.ads:8:15: warning: or (for some X => P and then Q) instead? semantics.ads:12:06: warning: function postcondition does not mention result semantics.ads:18:06: warning: function postcondition does not mention result semantics.ads:24:06: warning: function postcondition does not mention result semantics.ads:26:11: warning: suspicious expression semantics.ads:26:11: warning: did you mean (for all X => (if P then Q)) semantics.ads:26:11: warning: or (for some X => P and then Q) instead? semantics.ads:30:06: warning: function postcondition does not mention result semantics.ads:34:06: warning: function postcondition does not mention result Tested on x86_64-pc-linux-gnu, committed on trunk 2013-04-25 Hristian Kirtchev * sem_ch4.adb (Analyze_Quantified_Expression): Warn on a suspicious use of quantifier "some" when "all" was meant. (No_Else_Or_Trivial_True): New routine. Index: sem_ch4.adb =================================================================== --- sem_ch4.adb (revision 198275) +++ sem_ch4.adb (working copy) @@ -3501,13 +3501,15 @@ ----------------------------------- procedure Analyze_Quantified_Expression (N : Node_Id) is - QE_Scop : Entity_Id; - function Is_Empty_Range (Typ : Entity_Id) return Boolean; -- If the iterator is part of a quantified expression, and the range is -- known to be statically empty, emit a warning and replace expression -- with its static value. Returns True if the replacement occurs. + function No_Else_Or_Trivial_True (If_Expr : Node_Id) return Boolean; + -- Determine whether if expression If_Expr lacks an else part or if it + -- has one, it evaluates to True. + -------------------- -- Is_Empty_Range -- -------------------- @@ -3545,6 +3547,25 @@ end if; end Is_Empty_Range; + ----------------------------- + -- No_Else_Or_Trivial_True -- + ----------------------------- + + function No_Else_Or_Trivial_True (If_Expr : Node_Id) return Boolean is + Else_Expr : constant Node_Id := + Next (Next (First (Expressions (If_Expr)))); + begin + return + No (Else_Expr) + or else (Compile_Time_Known_Value (Else_Expr) + and then Is_True (Expr_Value (Else_Expr))); + end No_Else_Or_Trivial_True; + + -- Local variables + + Cond : constant Node_Id := Condition (N); + QE_Scop : Entity_Id; + -- Start of processing for Analyze_Quantified_Expression begin @@ -3579,11 +3600,29 @@ Preanalyze (Loop_Parameter_Specification (N)); end if; - Preanalyze_And_Resolve (Condition (N), Standard_Boolean); + Preanalyze_And_Resolve (Cond, Standard_Boolean); End_Scope; Set_Etype (N, Standard_Boolean); + + -- Diagnose a possible misuse of the "some" existential quantifier. When + -- we have a quantified expression of the form + -- + -- for some X => (if P then Q [else True]) + -- + -- the if expression will not hold and render the quantified expression + -- trivially True. + + if Formal_Extensions + and then not All_Present (N) + and then Nkind (Cond) = N_If_Expression + and then No_Else_Or_Trivial_True (Cond) + then + Error_Msg_N ("?suspicious expression", N); + Error_Msg_N ("\\did you mean (for all X ='> (if P then Q))", N); + Error_Msg_N ("\\or (for some X ='> P and then Q) instead'?", N); + end if; end Analyze_Quantified_Expression; -------------------