From patchwork Tue Dec 11 11:31:47 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: 1011049 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-492090-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="bUr5jSpU"; 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 43Dd8K52nrz9s3q for ; Tue, 11 Dec 2018 22:32:17 +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=ilDjaMY28u6klunPiT6579HMgxAug7QD3CKzO718zLjMb7RRMf rdEwJLLzjqRXEnM6tOYevi12dSRiXxZgWRIVsQk4a0yDPjd5IRtXA4aP6XlwunmX mWehrUAkgj7Ud2wKJfDT4rbmenk9+QH7HGo0f7zcYZMHGGUD/elEVASF4= 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=2bk8pdtrbGuB3PMekpQljz1TwAg=; b=bUr5jSpU0D0Q7C+2qblf JQUzdSpng/IzFXAfMjh4SnaG8WVun+yRLvP93ll5IcV05XQk65pozz8CxLSYhk1f ru6AmKSoPA5OS2a79hWaaA+PeYHVFjP+zBK2tcptidSASQu7DCrHfX9KanMA6ax3 xFIaKTO72yzh4X8e5kqB/wQ= Received: (qmail 66490 invoked by alias); 11 Dec 2018 11:31:52 -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 66393 invoked by uid 89); 11 Dec 2018 11:31:51 -0000 Authentication-Results: sourceware.org; auth=none 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, WEIRD_QUOTING autolearn=ham version=3.3.2 spammy=Reset, gnatprove, fashion, GNATprove 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, 11 Dec 2018 11:31:48 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 6C62656089; Tue, 11 Dec 2018 06:31:47 -0500 (EST) 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 xBKnaJNM-qyA; Tue, 11 Dec 2018 06:31:47 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 586A356088; Tue, 11 Dec 2018 06:31:47 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4862) id 576AC3573; Tue, 11 Dec 2018 06:31:47 -0500 (EST) Date: Tue, 11 Dec 2018 06:31:47 -0500 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Ed Schonberg Subject: [Ada] Spurious visibility error on aspect Predicate Message-ID: <20181211113147.GA104956@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes The GNAT-defined aspect Predicate has the same semantics as the Ada aspect Dynamic_Predicate, including direct visibility to the components of a record type to which the aspect applies. The following must compile quietly: gcc -c integer_stacks.ads ---- pragma SPARK_Mode (On); with Bounded_Stacks; package Integer_Stacks is new Bounded_Stacks (Element => Integer, Default_Element => 0); ---- generic type Element is private; Default_Element : Element; package Bounded_Stacks is type Stack (Capacity : Positive) is tagged private with Default_Initial_Condition => Empty (Stack); function "=" (Left, Right : Stack) return Boolean; function Extent (This : Stack) return Natural; function Empty (This : Stack) return Boolean; function Full (This : Stack) return Boolean; procedure Reset (This : out Stack) with Post'Class => Empty (This) and not Full (This), Global => null, Depends => (This =>+ null); procedure Push (This : in out Stack; Item : Element) with Pre'Class => not Full (This) and Extent (This) < This.Capacity, Post'Class => not Empty (This) and Extent (This) = Extent (This'Old) + 1, Global => null, Depends => (This =>+ Item); procedure Pop (This : in out Stack; Item : out Element) with Pre'Class => not Empty (This), Post'Class => not Full (This) and Extent (This) = Extent (This'Old) - 1, Global => null, Depends => (This =>+ null, Item => This); function Peek (This : Stack) return Element with Pre'Class => not Empty (This), Global => null, Depends => (Peek'Result => This); private type Contents is array (Positive range <>) of Element; type Stack (Capacity : Positive) is tagged record Values : Contents (1 .. Capacity); -- := (others => Default_Element); -- Top : Natural; Top : Natural := 0; end record with Predicate => Top <= Capacity, Annotate => (GNATprove, Intentional, "type ""Stack"" is not fully initialized", "Because zeroing Top is sufficient"); end Bounded_Stacks; ---- package body Bounded_Stacks is ------------ -- Extent -- ------------ function Extent (This : Stack) return Natural is (This.Top); ----------- -- Empty -- ----------- function Empty (This : Stack) return Boolean is (This.Top = 0); ---------- -- Full -- ---------- function Full (This : Stack) return Boolean is (This.Top = This.Capacity); ----------- -- Reset -- ----------- procedure Reset (This : out Stack) is begin This := (This.Capacity, Top => 0, others => <>); -- This.Top := 0; end Reset; ---------- -- Push -- ---------- procedure Push (This : in out Stack; Item : Element) is begin This.Top := This.Top + 1; This.Values (This.Top) := Item; end Push; --------- -- Pop -- --------- procedure Pop (This : in out Stack; Item : out Element) is begin Item := This.Values (This.Top); This.Top := This.Top - 1; end Pop; ---------- -- Peek -- ---------- function Peek (This : Stack) return Element is (This.Values (This.Top)); --------- -- "=" -- --------- function "=" (Left, Right : Stack) return Boolean is begin if Left.Top /= Right.Top then return False; else for K in 1 .. Left.Top loop if Left.Values (K) /= Right.Values (K) then return False; end if; end loop; return True; end if; end "="; end Bounded_Stacks; ---- Tested on x86_64-pc-linux-gnu, committed on trunk 2018-12-11 Ed Schonberg gcc/ada/ * sem_ch13.adb (Check_Aspect_At_End_Of_Declarations, Freeze_Entity_Checks): Process aspect Predicate in the same fashion as aspect Dynamic_Predicate. --- gcc/ada/sem_ch13.adb +++ gcc/ada/sem_ch13.adb @@ -9364,6 +9364,7 @@ package body Sem_Ch13 is -- components and discriminants of the type. elsif A_Id = Aspect_Dynamic_Predicate + or else A_Id = Aspect_Predicate or else A_Id = Aspect_Priority then Push_Type (Ent); @@ -11252,6 +11253,7 @@ package body Sem_Ch13 is then A_Id := Get_Aspect_Id (Ritem); if A_Id = Aspect_Dynamic_Predicate + or else A_Id = Aspect_Predicate or else A_Id = Aspect_Priority then -- Retrieve the visibility to components and discriminants