From patchwork Wed Aug 21 08:31:42 2019 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: 1150700 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-507429-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="WaXEmGKq"; 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 46D1CC277Pz9sBp for ; Wed, 21 Aug 2019 18:33:27 +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=EJ9at8Li6kYnF5+J2GkZU+1F/yz87Ls4MwOgwIpdlqzVPL5eO7 YtBQBhWPlFXC8iqVLOQz7yVb0UrHFMJeEBSrAeZ6VFHk+9w8IapIWnYaMesHgMzw 65Z6uw0JHITEacJslOp1yiWiQPGbri1M0SfNMlaVUvdTo/dFXdzrOTWIc= 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=6/TwOPbpVsw+A//3IGF6O4HXpS0=; b=WaXEmGKqlqELoL2B4EgM dVL/NEO5zmteWOVLWHkLWbWgNtpBAh8cDMZxcPWkszz3C1CDLR29EdKPF1rO1xlU +fUUv1IFeBg90kWD/IKjQzkNOdSeg1AWjVx4c6soUcRXaFaWoXcFc7uPhycSsGUc u81WRuwUJXHtQPWYXYUqZ8I= Received: (qmail 96465 invoked by alias); 21 Aug 2019 08:31:53 -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 96410 invoked by uid 89); 21 Aug 2019 08:31:52 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-10.8 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, SPF_NEUTRAL autolearn=ham version=3.3.1 spammy=HX-Languages-Length:736, UD:checks.adb, checks.adb, checksadb X-HELO: eggs.gnu.org Received: from eggs.gnu.org (HELO eggs.gnu.org) (209.51.188.92) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Wed, 21 Aug 2019 08:31:51 +0000 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1i0M20-00013J-5L for gcc-patches@gcc.gnu.org; Wed, 21 Aug 2019 04:31:50 -0400 Received: from rock.gnat.com ([2620:20:4000:0:a9e:1ff:fe9b:1d1]:56175) by eggs.gnu.org with esmtps (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.71) (envelope-from ) id 1i0M1y-000113-9y for gcc-patches@gcc.gnu.org; Wed, 21 Aug 2019 04:31:46 -0400 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 8264B1163F7; Wed, 21 Aug 2019 04:31:42 -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 um+SxR97Kd2p; Wed, 21 Aug 2019 04:31:42 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 7239D1163EA; Wed, 21 Aug 2019 04:31:42 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 70FC8646; Wed, 21 Aug 2019 04:31:42 -0400 (EDT) Date: Wed, 21 Aug 2019 04:31:42 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Avoid spurious error in GNATprove mode on non-null access types Message-ID: <20190821083142.GA71850@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-detected-operating-system: by eggs.gnu.org: GNU/Linux 3.x [fuzzy] X-Received-From: 2620:20:4000:0:a9e:1ff:fe9b:1d1 X-IsSubscribed: yes GNATprove directly handles non-null access checks, and requires that the frontend does not insert explicit checks in the form of conditional exceptions being raised. Now fixed. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2019-08-21 Yannick Moy gcc/ada/ * checks.adb (Install_Null_Excluding_Check): Do not install check in GNATprove mode. --- gcc/ada/checks.adb +++ gcc/ada/checks.adb @@ -7964,6 +7964,12 @@ package body Checks is return; end if; + -- In GNATprove mode, we do not apply the check + + if GNATprove_Mode then + return; + end if; + -- Otherwise install access check Insert_Action (N,