[Ada] Spurious error on unused Part_Of constituent

This patch updates the analysis of indicator Part_Of (or the lack thereof), to
ignore generic formal parameters for purposes of determining the visible state
space because they are not visible outside the generic and related instances.

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

--  gen_pack.ads

generic
   In_Formal     : in     Integer := 0;
   In_Out_Formal : in out Integer;

package Gen_Pack is
   Exported_In_Formal     : Integer renames In_Formal;
   Exported_In_Out_Formal : Integer renames In_Out_Formal;

end Gen_Pack;

--  pack.ads

with Gen_Pack;

package Pack
  with Abstract_State => State
is
   procedure Force_Body;

   Val : Integer;

private
   package OK_1 is
     new Gen_Pack (In_Out_Formal => Val)
   with Part_Of => State;                                            --  OK

   package OK_2 is
     new Gen_Pack (In_Formal => 1, In_Out_Formal => Val)
   with Part_Of => State;                                            --  OK

   package Error_1 is                                                --  Error
     new Gen_Pack (In_Out_Formal => Val);
   package Error_2 is                                                --  Error
     new Gen_Pack (In_Formal => 2, In_Out_Formal => Val);
end Pack;

--  pack.adb

package body Pack
  with Refined_State =>                                              --  Error
         (State => (OK_1.Exported_In_Formal,
                    OK_1.Exported_In_Out_Formal))
is
   procedure Force_Body is null;
end Pack;

--  gen_pack.ads

generic
   In_Formal     : in     Integer := 0;
   In_Out_Formal : in out Integer;

package Gen_Pack is
   Exported_In_Formal     : Integer renames In_Formal;
   Exported_In_Out_Formal : Integer renames In_Out_Formal;

end Gen_Pack;

--  pack.ads

with Gen_Pack;

package Pack
  with Abstract_State => State
is
   procedure Force_Body;

   Val : Integer;

private
   package OK_1 is
     new Gen_Pack (In_Out_Formal => Val)
   with Part_Of => State;                                            --  OK

   package OK_2 is
     new Gen_Pack (In_Formal => 1, In_Out_Formal => Val)
   with Part_Of => State;                                            --  OK

   package Error_1 is                                                --  Error
     new Gen_Pack (In_Out_Formal => Val);
   package Error_2 is                                                --  Error
     new Gen_Pack (In_Formal => 2, In_Out_Formal => Val);
end Pack;

--  pack.adb

package body Pack
  with Refined_State =>                                              --  Error
         (State => (OK_1.Exported_In_Formal,
                    OK_1.Exported_In_Out_Formal))
is
   procedure Force_Body is null;
end Pack;

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

$ gcc -c pack.adb
pack.adb:3:11: state "State" has unused Part_Of constituents
pack.adb:3:11: constant "Exported_In_Formal" defined at gen_pack.ads:6,
  instance at pack.ads:15
pack.adb:3:11: variable "Exported_In_Out_Formal" defined at gen_pack.ads:7,
  instance at pack.ads:15
pack.ads:19:12: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:19:12: "Error_1" is declared in the private part of package "Pack"
pack.ads:21:12: indicator Part_Of is required in this context (SPARK RM
  7.2.6(2))
pack.ads:21:12: "Error_2" is declared in the private part of package "Pack"

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

gcc/ada/

	* sem_prag.adb (Has_Visible_State): Do not consider generic formals
	because they are not part of the visible state space. Add constants to
	the list of acceptable visible states.
	(Propagate_Part_Of): Do not consider generic formals when propagating
	the Part_Of indicator.
	* sem_util.adb (Entity_Of): Do not follow renaming chains which go
	through a generic formal because they are not visible for SPARK
	purposes.
	* sem_util.ads (Entity_Of): Update the comment on usage.

From-SVN: r262768

4 files changed, 55 insertions, 15 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index ad067f6..b322861 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,15 @@
+2018-07-17  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Has_Visible_State): Do not consider generic formals
+	because they are not part of the visible state space. Add constants to
+	the list of acceptable visible states.
+	(Propagate_Part_Of): Do not consider generic formals when propagating
+	the Part_Of indicator.
+	* sem_util.adb (Entity_Of): Do not follow renaming chains which go
+	through a generic formal because they are not visible for SPARK
+	purposes.
+	* sem_util.ads (Entity_Of): Update the comment on usage.
+
 2018-07-17  Ed Schonberg  <schonberg@adacore.com>
 
 	* sem_util.adb (Gather_Components): A discriminant of an ancestor may
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 6bd5462..37b7d23 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19982,6 +19982,13 @@ package body Sem_Prag is
                      if not Comes_From_Source (Item_Id) then
                         null;
 
+                     --  Do not consider generic formals or their corresponding
+                     --  actuals because they are not part of a visible state.
+                     --  Note that both entities are marked as hidden.
+
+                     elsif Is_Hidden (Item_Id) then
+                        null;
+
                      --  The Part_Of indicator turns an abstract state or an
                      --  object into a constituent of the encapsulating state.
 
@@ -28775,9 +28782,19 @@ package body Sem_Prag is
             if not Comes_From_Source (Item_Id) then
                null;
 
+            --  Do not consider generic formals or their corresponding actuals
+            --  because they are not part of a visible state. Note that both
+            --  entities are marked as hidden.
+
+            elsif Is_Hidden (Item_Id) then
+               null;
+
             --  A visible state has been found
 
-            elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
+            elsif Ekind_In (Item_Id, E_Abstract_State,
+                                     E_Constant,
+                                     E_Variable)
+            then
                return True;
 
             --  Recursively peek into nested packages and instantiations
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 2b96ce8..0977392 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -7442,7 +7442,17 @@ package body Sem_Util is
             --    Ren : ... renames Obj;
 
             if Is_Entity_Name (Ren) then
-               Id := Entity (Ren);
+
+               --  Do not follow a renaming that goes through a generic formal,
+               --  because these entities are hidden and must not be referenced
+               --  from outside the generic.
+
+               if Is_Hidden (Entity (Ren)) then
+                  exit;
+
+               else
+                  Id := Entity (Ren);
+               end if;
 
             --  The reference renames a function result. Check the original
             --  node in case expansion relocates the function call.
@@ -8819,7 +8829,7 @@ package body Sem_Util is
                --  Stored_Constraint as well.
 
                --  An inherited discriminant may have been constrained in a
-               --  later ancestor (no the immediate parent) so we must examine
+               --  later ancestor (not the immediate parent) so we must examine
                --  the stored constraint of all of them to locate the inherited
                --  value.
 
@@ -8858,7 +8868,7 @@ package body Sem_Util is
                         end loop;
                      end if;
 
-                     --  Discriminant may be inherited from ancestor.
+                     --  Discriminant may be inherited from ancestor
                      T := Etype (T);
                   end loop;
                end;
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index 34d618e..21a74ae 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -126,8 +126,8 @@ package Sem_Util is
       Loc    : Source_Ptr := No_Location;
       Rep    : Boolean    := True;
       Warn   : Boolean    := False);
-   --  N is a subexpression which will raise constraint error when evaluated
-   --  at runtime. Msg is a message that explains the reason for raising the
+   --  N is a subexpression that will raise Constraint_Error when evaluated
+   --  at run time. Msg is a message that explains the reason for raising the
    --  exception. The last character is ? if the message is always a warning,
    --  even in Ada 95, and is not a ? if the message represents an illegality
    --  (because of violation of static expression rules) in Ada 95 (but not
@@ -614,19 +614,19 @@ package Sem_Util is
    --  Emit an error if iterated component association N is actually an illegal
    --  quantified expression lacking a quantifier.
 
-   function Dynamic_Accessibility_Level (Expr : Node_Id) return Node_Id;
-   --  Expr should be an expression of an access type. Builds an integer
-   --  literal except in cases involving anonymous access types where
-   --  accessibility levels are tracked at runtime (access parameters and Ada
-   --  2012 stand-alone objects).
-
    function Discriminated_Size (Comp : Entity_Id) return Boolean;
    --  If a component size is not static then a warning will be emitted
    --  in Ravenscar or other restricted contexts. When a component is non-
    --  static because of a discriminant constraint we can specialize the
    --  warning by mentioning discriminants explicitly. This was created for
    --  private components of protected objects, but is generally useful when
-   --  retriction (No_Implicit_Heap_Allocation) is active.
+   --  restriction No_Implicit_Heap_Allocation is active.
+
+   function Dynamic_Accessibility_Level (Expr : Node_Id) return Node_Id;
+   --  Expr should be an expression of an access type. Builds an integer
+   --  literal except in cases involving anonymous access types, where
+   --  accessibility levels are tracked at run time (access parameters and
+   --  Ada 2012 stand-alone objects).
 
    function Effective_Extra_Accessibility (Id : Entity_Id) return Entity_Id;
    --  Same as Einfo.Extra_Accessibility except thtat object renames
@@ -705,7 +705,8 @@ package Sem_Util is
    function Entity_Of (N : Node_Id) return Entity_Id;
    --  Obtain the entity of arbitrary node N. If N is a renaming, return the
    --  entity of the earliest renamed source abstract state or whole object.
-   --  If no suitable entity is available, return Empty.
+   --  If no suitable entity is available, return Empty. This routine carries
+   --  out actions that are tied to SPARK semantics.
 
    procedure Explain_Limited_Type (T : Entity_Id; N : Node_Id);
    --  This procedure is called after issuing a message complaining about an
@@ -2025,7 +2026,7 @@ package Sem_Util is
 
    function Is_Transfer (N : Node_Id) return Boolean;
    --  Returns True if the node N is a statement which is known to cause an
-   --  unconditional transfer of control at runtime, i.e. the following
+   --  unconditional transfer of control at run time, i.e. the following
    --  statement definitely will not be executed.
 
    function Is_True (U : Uint) return Boolean;