From patchwork Mon Oct 9 19:59:44 2017 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: 823467 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-463809-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="AXAOE081"; 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 3y9rgd1X21z9rxl for ; Tue, 10 Oct 2017 06:59:57 +1100 (AEDT) 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=Cs752XnWpIm2dJ7xAMGvDDx3+xXsHbyKQ2MCK4ysvNaUVbk4GZ 4EPhnNToy4UdYOWdfX1greapB0QkteyjhiLxbnuZhSl+zSeL1lsVPIVGLpsHLu1I wCuEoxDY9HGy3+fqF98DX1iW1bJr77tBDZmKXfJ9SoeRVmWEdaPLAwYq0= 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=d807zHCGg5xfnsfFfwRCbVv0hIc=; b=AXAOE08195HDdnEGAs6E oZCdtlzw//ox87MIkXyPEcHMOmIEjtDNFib3dzLaOsOoiqAXLMOaFAAt1MuI4QI/ 52cJz/hCB32gUyVdgPjQC/GmeN/065sBa/JF8zy/fzE/6WfBV9fVLrezpG60HDUY aLk0KEUhFwPZtMo8T0zAPD8= Received: (qmail 13790 invoked by alias); 9 Oct 2017 19:59:48 -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 13775 invoked by uid 89); 9 Oct 2017 19:59:47 -0000 Authentication-Results: sourceware.org; auth=none X-Virus-Found: No X-Spam-SWARE-Status: No, score=-11.9 required=5.0 tests=AWL, BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy= 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, 09 Oct 2017 19:59:46 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id A75935631C; Mon, 9 Oct 2017 15:59:44 -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 0WZCrEIo4alz; Mon, 9 Oct 2017 15:59:44 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 8E850561D5; Mon, 9 Oct 2017 15:59:44 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 8D8D443A; Mon, 9 Oct 2017 15:59:44 -0400 (EDT) Date: Mon, 9 Oct 2017 15:59:44 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Hristian Kirtchev Subject: [Ada] Suppress generation of ABE checks in GNATprove mode Message-ID: <20171009195944.GA43490@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes This patch suppresses the generation of ABE checks when compiling for GNATprove because a) the checks are not needed and b) the checks involve raise statements which are not supported by GNATprove. No need for a test. Tested on x86_64-pc-linux-gnu, committed on trunk 2017-10-09 Hristian Kirtchev * sem_elab.adb (Install_ABE_Check): Do not generate an ABE check for GNATprove. (Install_ABE_Failure): Do not generate an ABE failure for GNATprove. Index: sem_elab.adb =================================================================== --- sem_elab.adb (revision 253559) +++ sem_elab.adb (working copy) @@ -4199,9 +4199,15 @@ Scop_Id : Entity_Id; begin + -- Nothing to do when compiling for GNATprove because raise statements + -- are not supported. + + if GNATprove_Mode then + return; + -- Nothing to do when the compilation will not produce an executable - if Serious_Errors_Detected > 0 then + elsif Serious_Errors_Detected > 0 then return; -- Nothing to do for a compilation unit because there is no executable @@ -4325,9 +4331,15 @@ -- Start for processing for Install_ABE_Check begin + -- Nothing to do when compiling for GNATprove because raise statements + -- are not supported. + + if GNATprove_Mode then + return; + -- Nothing to do when the compilation will not produce an executable - if Serious_Errors_Detected > 0 then + elsif Serious_Errors_Detected > 0 then return; -- Nothing to do when the target is a protected subprogram because the @@ -4381,9 +4393,15 @@ Scop_Id : Entity_Id; begin + -- Nothing to do when compiling for GNATprove because raise statements + -- are not supported. + + if GNATprove_Mode then + return; + -- Nothing to do when the compilation will not produce an executable - if Serious_Errors_Detected > 0 then + elsif Serious_Errors_Detected > 0 then return; -- Do not install an ABE check for a compilation unit because there is