From patchwork Mon Jun 11 09:22:05 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 927537 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-479433-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="nHh2vtdN"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 4146x03XXRz9ryk for ; Mon, 11 Jun 2018 19:22:28 +1000 (AEST) 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=kI14qA2217MJfcjwN6B1sMmTLMJ86iQtcPZdAc8E7x6Qjo7CY6 Mx+/e95pc/8VRW7I6wOVZMhQPGEB+/30vsy3C4YyEDuqlTH2CUx8gm4ZqMXN5dWv wXf+9i6sc1hkNJDTbnZ2n11L39RhvyaJ40V8oMmwi6/OYbYkisMnVS2co= 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=y4J7EiGPDFRaBYBKIO7UJqTRZOc=; b=nHh2vtdNmp510n4rr9X/ SAPr40DAn1sBQn8M9aDcpVsppiPpr0yGAF38VTYeqDwjx4bCVN202rhuDbp9wotM a3BUZOMqUxS42jgMKHlGepBQLJjPZ/yfObaINdhdwL/TsCjxWjM1JHc2wVncPvPc ARAGsLnYe4D2Dk5OX6Xt3QU= Received: (qmail 20020 invoked by alias); 11 Jun 2018 09:22:09 -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 19809 invoked by uid 89); 11 Jun 2018 09:22:08 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.9 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=contracts, Hx-languages-length:1798, contract X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Mon, 11 Jun 2018 09:22:06 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 22B23560F3; Mon, 11 Jun 2018 05:22:05 -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 ODK+q8f7KSwK; Mon, 11 Jun 2018 05:22:05 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id 12623560EC; Mon, 11 Jun 2018 05:22:05 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 1165A54C; Mon, 11 Jun 2018 05:22:05 -0400 (EDT) Date: Mon, 11 Jun 2018 05:22:05 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [Ada] Fix handling of Pre/Post contracts with AND THEN expressions Message-ID: <20180611092204.GA134873@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes Pre- and postconditions with top-level AND THEN expressions are broken down into checks of indivudial conjuncts for more precise error reporting. This rewrite interfers with detection of potentially unevaluadted use of 'Old, e.g. a contract like "Pre => Foo and then Bar" is rewritten into a two pragmas Check, for expressions "Foo" and "Bar", but the latter remains potentially unevaluted. This patch fixes detection of the AND THEN rewrite. This fixes inlining in the GNATprove mode, i.e. the following testc case must not emit a warning like: contract1.adb:14:07: info: no contextual analysis of "Foo" (in potentially unevaluated context) Tested on x86_64-pc-linux-gnu, committed on trunk 2018-06-11 Piotr Trojanek gcc/ada/ * sem_util.adb (Is_Potentially_Unevaluated): Fix detection of contracts with AND THEN expressions broken down into individual conjuncts. gcc/testsuite/ * gnat.dg/contract1.adb: New testcase. --- gcc/ada/sem_util.adb +++ gcc/ada/sem_util.adb @@ -16453,7 +16453,9 @@ package body Sem_Util is while Present (Par) and then Nkind (Par) /= N_Pragma_Argument_Association loop - if Nkind (Original_Node (Par)) = N_And_Then then + if Is_Rewrite_Substitution (Par) + and then Nkind (Original_Node (Par)) = N_And_Then + then return True; end if; --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/contract1.adb @@ -0,0 +1,20 @@ +-- { dg-do compile } +-- { dg-options "-gnatd.F -gnatwa" } + +with Ada.Dispatching; + +procedure Contract1 with SPARK_Mode is + + function Foo return Boolean is + begin + Ada.Dispatching.Yield; + return True; + end Foo; + + Dummy : constant Integer := 0; + +begin + if Foo and then True then + raise Program_Error; + end if; +end Contract1;