From d05bdd90e646234d08ceb855f9b4ae06896f4337 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 11 Jun 2018 09:18:01 +0000 Subject: [PATCH] [Ada] Do not force Part_Of on generic units 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. 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. From-SVN: r261412 --- gcc/ada/ChangeLog | 6 ++++ gcc/ada/sem_prag.adb | 28 +++++++++++-------- gcc/testsuite/ChangeLog | 8 ++++++ .../gnat.dg/part_of1-instantiation.adb | 10 +++++++ .../gnat.dg/part_of1-instantiation.ads | 6 ++++ .../gnat.dg/part_of1-private_generic.adb | 13 +++++++++ .../gnat.dg/part_of1-private_generic.ads | 12 ++++++++ gcc/testsuite/gnat.dg/part_of1.ads | 2 ++ 8 files changed, 73 insertions(+), 12 deletions(-) create mode 100644 gcc/testsuite/gnat.dg/part_of1-instantiation.adb create mode 100644 gcc/testsuite/gnat.dg/part_of1-instantiation.ads create mode 100644 gcc/testsuite/gnat.dg/part_of1-private_generic.adb create mode 100644 gcc/testsuite/gnat.dg/part_of1-private_generic.ads create mode 100644 gcc/testsuite/gnat.dg/part_of1.ads diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 00af9bebebe..3ab3de7d28c 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2018-06-11 Yannick Moy + + * 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. + 2018-06-11 Piotr Trojanek * sem_ch13.adb (Analyze_Aspect_Specifications): Don't split AND THEN diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 9cfb39c9ca2..3f58f570676 100644 --- a/gcc/ada/sem_prag.adb +++ b/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 diff --git a/gcc/testsuite/ChangeLog b/gcc/testsuite/ChangeLog index a34c710adbc..7e8948e3151 100644 --- a/gcc/testsuite/ChangeLog +++ b/gcc/testsuite/ChangeLog @@ -1,3 +1,11 @@ +2018-06-11 Yannick Moy + + * 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. + 2018-06-11 Piotr Trojanek * gnat.dg/contract1.adb: New testcase. diff --git a/gcc/testsuite/gnat.dg/part_of1-instantiation.adb b/gcc/testsuite/gnat.dg/part_of1-instantiation.adb new file mode 100644 index 00000000000..0efc1deb9aa --- /dev/null +++ b/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; diff --git a/gcc/testsuite/gnat.dg/part_of1-instantiation.ads b/gcc/testsuite/gnat.dg/part_of1-instantiation.ads new file mode 100644 index 00000000000..1ad8a2a25ce --- /dev/null +++ b/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; diff --git a/gcc/testsuite/gnat.dg/part_of1-private_generic.adb b/gcc/testsuite/gnat.dg/part_of1-private_generic.adb new file mode 100644 index 00000000000..ec1bba5e0b5 --- /dev/null +++ b/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; diff --git a/gcc/testsuite/gnat.dg/part_of1-private_generic.ads b/gcc/testsuite/gnat.dg/part_of1-private_generic.ads new file mode 100644 index 00000000000..f6aacb54c68 --- /dev/null +++ b/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; diff --git a/gcc/testsuite/gnat.dg/part_of1.ads b/gcc/testsuite/gnat.dg/part_of1.ads new file mode 100644 index 00000000000..edeabb2973a --- /dev/null +++ b/gcc/testsuite/gnat.dg/part_of1.ads @@ -0,0 +1,2 @@ +package Part_Of1 is +end Part_Of1; -- 2.30.2