[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 00af9bebebed1929450e92c63196013b0fa3ac69..3ab3de7d28c9126b8a83a2bde7628cf52fb6b14d 100644 (file)
--- 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 9cfb39c9ca2412db0f070c3bf6b6442a25b2ad44..3f58f570676704f9d16603c80e46655a5bb3d190 100644 (file)
--- 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 a34c710adbc81b172d14282ab564f73c1e7132aa..7e8948e3151879ee95177e7cd377e79fc30e67b7 100644 (file)
--- a/gcc/testsuite/ChangeLog
+++ b/gcc/testsuite/ChangeLog
@@ -1,3 +1,11 @@
+2018-06-11  Yannick Moy  <moy@adacore.com>
+
+       * 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  <trojanek@adacore.com>
 
        * 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 (file)
index 0000000..0efc1de
--- /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 (file)
index 0000000..1ad8a2a
--- /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 (file)
index 0000000..ec1bba5
--- /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 (file)
index 0000000..f6aacb5
--- /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 (file)
index 0000000..edeabb2
--- /dev/null
+++ b/gcc/testsuite/gnat.dg/part_of1.ads
@@ -0,0 +1,2 @@
+package Part_Of1 is
+end Part_Of1;