From patchwork Tue Oct 9 15:09:32 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: 981356 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-487212-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="bwuBsVkS"; 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 42V0z83rBKz9s55 for ; Wed, 10 Oct 2018 02:10:28 +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=OV0UYyuo2h23RUiZB3TQPNpupBu1r+w6Ogdru53G1TXR5EquSv Z99sKzCLZBhWB12pVxnqmus9GCqkOI9A0WWVMBOFpyxFIE3sxMBHR6BLnupsbFih uYZ92reegTrHjS1B3rReYdN3eBJDnSVjHuLtWKyiKCiS/5GK2NS5Lr+VU= 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=8XBXcT9ldxsKdl7toNKyMYvCmik=; b=bwuBsVkSRV+D9XIsCZ6D eK2qJKnyGNn/A9KyYwwFAz9yOxFj3/99UrdqoaZqK0kV97LeeadhhWL+T1kdAZTI AZB8BO02PGQrsedmlyKo8LFcFpKgtCJx7/CeUxNs0ejf7wmDMjX4mq+/Yz9GS802 8/YgUHBBcNuBQHiueUYKfiQ= Received: (qmail 30796 invoked by alias); 9 Oct 2018 15:09:36 -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 30648 invoked by uid 89); 9 Oct 2018 15:09:35 -0000 Authentication-Results: sourceware.org; auth=none 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=yannick, Yannick, moy 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; Tue, 09 Oct 2018 15:09:34 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 95B5456016; Tue, 9 Oct 2018 11:09:32 -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 6+-UMtAw983B; Tue, 9 Oct 2018 11:09:32 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 831B556012; Tue, 9 Oct 2018 11:09:32 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 821A634B3; Tue, 9 Oct 2018 11:09:32 -0400 (EDT) Date: Tue, 9 Oct 2018 11:09:32 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Ignore pragmas Compile_Time_Error/Warning in GNATprove mode Message-ID: <20181009150932.GA123371@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes GNATprove does not have sometimes the precise information of the compiler about size of types and objects, so that it cannot evaluate the expressions in pragma Compile_Time_Error/Warning the same way the compiler does. Thus, these pragmas should be ignored in GNATprove mode, as it can neither verify them nor assume them (if the expression cannot be evaluated at compile time, then the semantics for GNAT is to ignore them). Tested on x86_64-pc-linux-gnu, committed on trunk 2018-10-09 Yannick Moy gcc/ada/ * sem_prag.adb (Process_Compile_Time_Warning_Or_Error): Rewrite pragmas as null statements in GNATprove mode. --- gcc/ada/sem_prag.adb +++ gcc/ada/sem_prag.adb @@ -7570,6 +7570,17 @@ package body Sem_Prag is -- Start of processing for Process_Compile_Time_Warning_Or_Error begin + -- In GNATprove mode, pragmas Compile_Time_Error and + -- Compile_Time_Warning are ignored, as the analyzer may not have the + -- same information as the compiler (in particular regarding size of + -- objects decided in gigi) so it makes no sense to issue an error or + -- warning in GNATprove. + + if GNATprove_Mode then + Rewrite (N, Make_Null_Statement (Loc)); + return; + end if; + Check_Arg_Count (2); Check_No_Identifiers; Check_Arg_Is_OK_Static_Expression (Arg2, Standard_String);