aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2018-06-11 09:18:01 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2018-06-11 09:18:01 +0000
commitd05bdd90e646234d08ceb855f9b4ae06896f4337 (patch)
treed7a6b30d80bf275e88483ae67d9eca7601cd65b8 /gcc/ada
parent270c6b4d6f9300f36cb7e06594d71a62ab59af0a (diff)
downloadgcc-d05bdd90e646234d08ceb855f9b4ae06896f4337.zip
gcc-d05bdd90e646234d08ceb855f9b4ae06896f4337.tar.gz
gcc-d05bdd90e646234d08ceb855f9b4ae06896f4337.tar.bz2
[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 <moy@adacore.com> 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
Diffstat (limited to 'gcc/ada')
-rw-r--r--gcc/ada/ChangeLog6
-rw-r--r--gcc/ada/sem_prag.adb28
2 files changed, 22 insertions, 12 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 00af9be..3ab3de7 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2018-06-11 Yannick Moy <moy@adacore.com>
+
+ * 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 <trojanek@adacore.com>
* 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 9cfb39c..3f58f57 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