[Ada] Spurious error on unused Part_Of constituent

[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