From patchwork Mon Jun 11 09:22:25 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: 927542 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-479435-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="MHnN5pZv"; 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 4146xS2sDtz9ryk for ; Mon, 11 Jun 2018 19:22: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=i0xHqjJBHa/rsgAlpoT9amHoJVguBb3OoVjg+mOJZHrE1gTM55 M4mTJ9kYQCdHA+IYmJtYkK/QRT3vyijrnn3MJBwRTeYPlacie0B4sHj6h3RJQCc/ Cf9Z8i4AlRW+VtziY+xN+XpF3h+Bz8Yt/4ATrGu5ajjqELkRU+ozSNbPk= 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=37ci8BZ5p6ic+/NnVapsUfEhcOY=; b=MHnN5pZvjYtZ4NZlpp3a OGuForcmxfYDEhr0fwb1mJFIPB/Xuch6NFgA6qPtKXW8Ec9TU1lucjnrzkhxIJha SFsRFr1rAbD4T8ga/Tc5JHXyy+/1k2rd7P+UOENOMOg2vZznqbg90AZdhNxKk8T1 plddw9LXvT+6Vf3zzXHjjjw= Received: (qmail 22570 invoked by alias); 11 Jun 2018 09:22:29 -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 22454 invoked by uid 89); 11 Jun 2018 09:22:28 -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=Numbers, nearest, Placement, State 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, 11 Jun 2018 09:22:26 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 4451E560ED; Mon, 11 Jun 2018 05:22:25 -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 IiKYLVZe29i4; Mon, 11 Jun 2018 05:22:25 -0400 (EDT) Received: from tron.gnat.com (tron.gnat.com [205.232.38.10]) by rock.gnat.com (Postfix) with ESMTP id 32FF9560EC; Mon, 11 Jun 2018 05:22:25 -0400 (EDT) Received: by tron.gnat.com (Postfix, from userid 4862) id 320AD54C; Mon, 11 Jun 2018 05:22:25 -0400 (EDT) Date: Mon, 11 Jun 2018 05:22:25 -0400 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Do not force Part_Of on generic units Message-ID: <20180611092225.GA134919@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes This fixes the code checking SPARK RM 7.2.6(3) so that generic child units are not forced to use Part_Of to relate their abstract state to the state of their parent. Tested on x86_64-pc-linux-gnu, committed on trunk 2018-06-11 Yannick Moy gcc/ada/ * sem_prag.adb (Analyze_Part_Of): Only allow Part_Of on non-generic unit. (Check_Missing_Part_Of): Do not force Part_Of on generic unit. gcc/testsuite/ * gnat.dg/part_of1-instantiation.adb, gnat.dg/part_of1-instantiation.ads, gnat.dg/part_of1-private_generic.adb, gnat.dg/part_of1-private_generic.ads, gnat.dg/part_of1.ads: New testcase. --- gcc/ada/sem_prag.adb +++ gcc/ada/sem_prag.adb @@ -3200,20 +3200,21 @@ package body Sem_Prag is -- The item appears in the visible state space of some package. In -- general this scenario does not warrant Part_Of except when the - -- package is a private child unit and the encapsulating state is - -- declared in a parent unit or a public descendant of that parent - -- unit. + -- package is a non-generic private child unit and the encapsulating + -- state is declared in a parent unit or a public descendant of that + -- parent unit. elsif Placement = Visible_State_Space then if Is_Child_Unit (Pack_Id) + and then not Is_Generic_Unit (Pack_Id) and then Is_Private_Descendant (Pack_Id) then -- A variable or state abstraction which is part of the visible - -- state of a private child unit or its public descendants must - -- have its Part_Of indicator specified. The Part_Of indicator - -- must denote a state declared by either the parent unit of - -- the private unit or by a public descendant of that parent - -- unit. + -- state of a non-generic private child unit or its public + -- descendants must have its Part_Of indicator specified. The + -- Part_Of indicator must denote a state declared by either the + -- parent unit of the private unit or by a public descendant of + -- that parent unit. -- Find the nearest private ancestor (which can be the current -- unit itself). @@ -3250,8 +3251,9 @@ package body Sem_Prag is return; end if; - -- Indicator Part_Of is not needed when the related package is not - -- a private child unit or a public descendant thereof. + -- Indicator Part_Of is not needed when the related package is + -- not a non-generic private child unit or a public descendant + -- thereof. else SPARK_Msg_N @@ -28831,11 +28833,13 @@ package body Sem_Prag is -- In general an item declared in the visible state space of a package -- does not require a Part_Of indicator. The only exception is when the - -- related package is a private child unit in which case Part_Of must - -- denote a state in the parent unit or in one of its descendants. + -- related package is a non-generic private child unit in which case + -- Part_Of must denote a state in the parent unit or in one of its + -- descendants. elsif Placement = Visible_State_Space then if Is_Child_Unit (Pack_Id) + and then not Is_Generic_Unit (Pack_Id) and then Is_Private_Descendant (Pack_Id) then -- A package instantiation does not need a Part_Of indicator when --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/part_of1-instantiation.adb @@ -0,0 +1,10 @@ +-- { dg-do compile } + +with Part_Of1.Private_Generic; + +package body Part_Of1.Instantiation +with + Refined_State => (State => Inst.State) +is + package Inst is new Part_Of1.Private_Generic; +end Part_Of1.Instantiation; --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/part_of1-instantiation.ads @@ -0,0 +1,6 @@ +package Part_Of1.Instantiation +with + Abstract_State => State +is + pragma Elaborate_Body; +end Part_Of1.Instantiation; --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/part_of1-private_generic.adb @@ -0,0 +1,13 @@ +package body Part_Of1.Private_Generic +with + Refined_State => (State => Numbers) +is + Numbers : array (Range_Type) of Integer := (others => 0); + + function Get (I : Range_Type) return Integer + is + begin + return Numbers (I); + end Get; + +end Part_Of1.Private_Generic; --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/part_of1-private_generic.ads @@ -0,0 +1,12 @@ +private generic + Count : Integer := 4; +package Part_Of1.Private_Generic +with + Abstract_State => State +is + + subtype Range_Type is Integer range 1 .. Count; + + function Get (I : Range_Type) return Integer; + +end Part_Of1.Private_Generic; --- /dev/null new file mode 100644 +++ gcc/testsuite/gnat.dg/part_of1.ads @@ -0,0 +1,2 @@ +package Part_Of1 is +end Part_Of1;