From patchwork Wed May 30 09:00:40 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: 922634 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-478739-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="TFQ3DXXo"; 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 40wl2m6DRSz9s1R for ; Wed, 30 May 2018 19:01:52 +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=tFFb6lp7iHMy0H/v6JVMnXu+APBgiroMgUeuLVZjyDZHXlD8oh A6QWWi26haFxzVSA6VFSoG4A5PNqAmjk+5J2k3SscJ+Ou8CPRRATqwmOFEaUMJOT cFWp9vYBx+wUSst2flHgG751gFBDqFrxTZQCQPUxpRZOCwYjlsQxAE1Pk= 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=iO2puyTKEpyxQG20dm9//B9q0nE=; b=TFQ3DXXo6zM41psjX0E8 je4xHRTokbjuhHEEZopuRusiq1H1Y7y9JteP4rs1WIOVJY8hH0eORBbJMy82Boys qlzsytTeY1sUYvG3kvahpegHwAWj04JfxbTjN6TPSRZFohZuGOp/m401qWdd7KZs ixVlq+kH+PxaG9PVzFAPamE= Received: (qmail 85044 invoked by alias); 30 May 2018 09:00:54 -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 83726 invoked by uid 89); 30 May 2018 09:00:48 -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=Hx-languages-length:1107 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; Wed, 30 May 2018 09:00:42 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 10502117F48; Wed, 30 May 2018 05:00:41 -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 OTqZGvFPqyo5; Wed, 30 May 2018 05:00:41 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id F34D9117F0B; Wed, 30 May 2018 05:00:40 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id F06CA78A; Wed, 30 May 2018 05:00:40 -0400 (EDT) Date: Wed, 30 May 2018 05:00:40 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Correctly ignore Assertion_Policy in modes CodePeer and GNATprove Message-ID: <20180530090040.GA22601@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes In the modes for static analysis with CodePeer or formal verification with GNATprove, the value of Assertion_Policy for a given policy is ignored if it's not Disable, as CodePeer/GNATprove are meant to check assertions even when not enabled at run time. This was not done consistently, which could lead to spurious errors on policy mismatch on ghost code inside assertions. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2018-05-30 Yannick Moy gcc/ada/ * sem_util.adb (Policy_In_Effect): Take into account CodePeer and GNATprove modes. --- gcc/ada/sem_util.adb +++ gcc/ada/sem_util.adb @@ -22487,6 +22487,16 @@ package body Sem_Util is end if; end if; + -- In CodePeer mode and GNATprove mode, we need to consider all + -- assertions, unless they are disabled. Force Name_Check on + -- ignored assertions. + + if Nam_In (Kind, Name_Ignore, Name_Off) + and then (CodePeer_Mode or GNATprove_Mode) + then + Kind := Name_Check; + end if; + return Kind; end Policy_In_Effect;