[Ada] Missing error on hidden state in instantiation

This patch modifies the analysis of package contracts to split processing
which is specific to package instantiations on its own. As a result, the
lack of indicator Part_Of can now be properly assessed.

------------
-- Source --
------------

--  gen_pack.ads

generic
package Gen_Pack is
   Pack_Var : Integer := 1;
end Gen_Pack;

--  gen_wrap.ads

with Gen_Pack;

generic
package Gen_Wrap is
   Wrap_Var : Integer := 1;

   package Inst is new Gen_Pack;
end Gen_Wrap;

--  pack.ads

with Gen_Pack;
with Gen_Wrap;

package Pack
  with SPARK_Mode     => On,
       Abstract_State => State
is
   procedure Force_Body;

private
   package OK_Inst_1 is new Gen_Pack                                 --  OK
     with Part_Of => State;                                          --  OK

   package OK_Inst_2 is new Gen_Pack;                                --  OK
   pragma Part_Of (State);                                           --  OK

   package OK_Inst_3 is new Gen_Wrap                                 --  OK
     with Part_Of => State;                                          --  OK

   package OK_Inst_4 is new Gen_Wrap;                                --  OK
   pragma Part_Of (State);

   package Error_Inst_1 is new Gen_Pack;                             --  Error
   package Error_Inst_2 is new Gen_Wrap;                             --  Error
end Pack;

--  pack.adb

package body Pack
  with SPARK_Mode    => On,
       Refined_State =>
         (State => (OK_Inst_1.Pack_Var, OK_Inst_2.Pack_Var,
                    OK_Inst_3.Wrap_Var, OK_Inst_3.Inst.Pack_Var,
                    OK_Inst_4.Wrap_Var, OK_Inst_4.Inst.Pack_Var))
is
   procedure Force_Body is null;
end Pack;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c pack.adb
pack.ads:23:12: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:23:12: "Error_Inst_1" is declared in the private part of package
  "Pack"
pack.ads:24:12: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:24:12: "Error_Inst_2" is declared in the private part of package
  "Pack"

2018-07-16  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* contracts.adb (Analyze_Contracts): Add specialized processing for
	package instantiation contracts.
	(Analyze_Package_Contract): Remove the verification of a missing
	Part_Of indicator.
	(Analyze_Package_Instantiation_Contract): New routine.
	* contracts.ads (Analyze_Package_Contract): Update the comment on
	usage.
	* sem_prag.adb (Check_Missing_Part_Of): Ensure that the entity of the
	instance is being examined when trying to determine whether a package
	instantiation needs a Part_Of indicator.

From-SVN: r262731

4 files changed, 92 insertions, 15 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 6909066..a72e80f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,18 @@
 2018-07-16  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* contracts.adb (Analyze_Contracts): Add specialized processing for
+	package instantiation contracts.
+	(Analyze_Package_Contract): Remove the verification of a missing
+	Part_Of indicator.
+	(Analyze_Package_Instantiation_Contract): New routine.
+	* contracts.ads (Analyze_Package_Contract): Update the comment on
+	usage.
+	* sem_prag.adb (Check_Missing_Part_Of): Ensure that the entity of the
+	instance is being examined when trying to determine whether a package
+	instantiation needs a Part_Of indicator.
+
+2018-07-16  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* einfo.adb, exp_ch7.adb, exp_ch9.adb, exp_unst.adb, inline.adb,
 	sem.adb, sem_ch12.adb, sem_ch13.adb, sem_ch3.adb, sem_eval.adb,
 	sem_util.adb: Minor reformatting.
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 104fd16..69cece9 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -53,6 +53,13 @@ with Tbuild;   use Tbuild;
 
 package body Contracts is
 
+   procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id);
+   --  Analyze all delayed pragmas chained on the contract of package
+   --  instantiation Inst_Id as if they appear at the end of a declarative
+   --  region. The pragmas in question are:
+   --
+   --    Part_Of
+
    procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id);
    --  (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
    --  contract-only subprogram body of eligible subprograms found in L, adds
@@ -386,6 +393,11 @@ package body Contracts is
          elsif Nkind (Decl) = N_Object_Declaration then
             Analyze_Object_Contract (Defining_Entity (Decl));
 
+         --  Package instantiation
+
+         elsif Nkind (Decl) = N_Package_Instantiation then
+            Analyze_Package_Instantiation_Contract (Defining_Entity (Decl));
+
          --  Protected units
 
          elsif Nkind_In (Decl, N_Protected_Type_Declaration,
@@ -1074,17 +1086,6 @@ package body Contracts is
          end if;
       end if;
 
-      --  Check whether the lack of indicator Part_Of agrees with the placement
-      --  of the package instantiation with respect to the state space.
-
-      if Is_Generic_Instance (Pack_Id) then
-         Prag := Get_Pragma (Pack_Id, Pragma_Part_Of);
-
-         if No (Prag) then
-            Check_Missing_Part_Of (Pack_Id);
-         end if;
-      end if;
-
       --  Restore the SPARK_Mode of the enclosing context after all delayed
       --  pragmas have been analyzed.
 
@@ -1100,6 +1101,62 @@ package body Contracts is
       end if;
    end Analyze_Package_Contract;
 
+   --------------------------------------------
+   -- Analyze_Package_Instantiation_Contract --
+   --------------------------------------------
+
+   --  WARNING: This routine manages SPARK regions. Return statements must be
+   --  replaced by gotos which jump to the end of the routine and restore the
+   --  SPARK mode.
+
+   procedure Analyze_Package_Instantiation_Contract (Inst_Id : Entity_Id) is
+      Inst_Spec : constant Node_Id :=
+                    Instance_Spec (Unit_Declaration_Node (Inst_Id));
+
+      Saved_SM  : constant SPARK_Mode_Type := SPARK_Mode;
+      Saved_SMP : constant Node_Id         := SPARK_Mode_Pragma;
+      --  Save the SPARK_Mode-related data to restore on exit
+
+      Pack_Id : Entity_Id;
+      Prag    : Node_Id;
+
+   begin
+      --  Nothing to do when the package instantiation is erroneous or left
+      --  partially decorated.
+
+      if No (Inst_Spec) then
+         return;
+      end if;
+
+      Pack_Id := Defining_Entity (Inst_Spec);
+      Prag    := Get_Pragma (Pack_Id, Pragma_Part_Of);
+
+      --  Due to the timing of contract analysis, delayed pragmas may be
+      --  subject to the wrong SPARK_Mode, usually that of the enclosing
+      --  context. To remedy this, restore the original SPARK_Mode of the
+      --  related package.
+
+      Set_SPARK_Mode (Pack_Id);
+
+      --  Check whether the lack of indicator Part_Of agrees with the placement
+      --  of the package instantiation with respect to the state space. Nested
+      --  package instantiations do not need to be checked because they inherit
+      --  Part_Of indicator of the outermost package instantiation (see routine
+      --  Propagate_Part_Of in Sem_Prag).
+
+      if In_Instance then
+         null;
+
+      elsif No (Prag) then
+         Check_Missing_Part_Of (Pack_Id);
+      end if;
+
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
+      Restore_SPARK_Mode (Saved_SM, Saved_SMP);
+   end Analyze_Package_Instantiation_Contract;
+
    --------------------------------
    -- Analyze_Protected_Contract --
    --------------------------------
diff --git a/gcc/ada/contracts.ads b/gcc/ada/contracts.ads
index 4a0997f..46f52d1 100644
--- a/gcc/ada/contracts.ads
+++ b/gcc/ada/contracts.ads
@@ -35,6 +35,7 @@ package Contracts is
    --  [generic] package, package body, protected unit, [generic] subprogram,
    --  subprogram body, variable or task unit denoted by Id. The following are
    --  valid pragmas:
+   --
    --    Abstract_State
    --    Async_Readers
    --    Async_Writers
@@ -66,6 +67,7 @@ package Contracts is
    --  Analyze all delayed pragmas chained on the contract of entry or
    --  subprogram body Body_Id as if they appeared at the end of a declarative
    --  region. Pragmas in question are:
+   --
    --    Contract_Cases   (stand alone subprogram body)
    --    Depends          (stand alone subprogram body)
    --    Global           (stand alone subprogram body)
@@ -82,6 +84,7 @@ package Contracts is
    --  Analyze all delayed pragmas chained on the contract of entry or
    --  subprogram Subp_Id as if they appeared at the end of a declarative
    --  region. The pragmas in question are:
+   --
    --    Contract_Cases
    --    Depends
    --    Global
@@ -98,6 +101,7 @@ package Contracts is
    --  Analyze all delayed pragmas chained on the contract of object Obj_Id as
    --  if they appeared at the end of the declarative region. The pragmas to be
    --  considered are:
+   --
    --    Async_Readers
    --    Async_Writers
    --    Depends           (single concurrent object)
@@ -115,6 +119,7 @@ package Contracts is
    --  Analyze all delayed pragmas chained on the contract of package body
    --  Body_Id as if they appeared at the end of a declarative region. The
    --  pragmas that are considered are:
+   --
    --    Refined_State
    --
    --  Freeze_Id is the entity of a [generic] package body or a [generic]
@@ -124,9 +129,9 @@ package Contracts is
    --  Analyze all delayed pragmas chained on the contract of package Pack_Id
    --  as if they appeared at the end of a declarative region. The pragmas
    --  that are considered are:
+   --
    --    Initial_Condition
    --    Initializes
-   --    Part_Of
 
    procedure Analyze_Protected_Contract (Prot_Id : Entity_Id);
    --  Analyze all delayed pragmas chained on the contract of protected unit
@@ -137,6 +142,7 @@ package Contracts is
    --  Analyze all delayed pragmas chained on the contract of subprogram body
    --  stub Stub_Id as if they appeared at the end of a declarative region. The
    --  pragmas in question are:
+   --
    --    Contract_Cases
    --    Depends
    --    Global
@@ -151,6 +157,7 @@ package Contracts is
    --  Analyze all delayed pragmas chained on the contract of task unit Task_Id
    --  as if they appeared at the end of a declarative region. The pragmas in
    --  question are:
+   --
    --    Depends
    --    Global
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index a88b37d..6bd5462 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -28897,9 +28897,9 @@ package body Sem_Prag is
          --  A package instantiation does not need a Part_Of indicator when the
          --  related generic template has no visible state.
 
-         elsif Ekind (Pack_Id) = E_Package
-           and then Is_Generic_Instance (Pack_Id)
-           and then not Has_Visible_State (Pack_Id)
+         elsif Ekind (Item_Id) = E_Package
+           and then Is_Generic_Instance (Item_Id)
+           and then not Has_Visible_State (Item_Id)
          then
             null;