[Ada] Spurious error on Part_Of indicator

This patch modifies the verification of a missing Part_Of indicator to avoid
considering constants as visible state of a package instantiation because the
compiler cannot determine whether their values depend on variable input. This
diagnostic is left to GNATprove.

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

--  gnat.adc

pragma SPARK_Mode;

--  gen_pack.ads

generic
package Gen_Pack is
   Val : constant Integer := 123;
end Gen_Pack;

--  pack.ads

with Gen_Pack;

package Pack
  with Abstract_State => Pack_State
is
   procedure Force_Body;
private
   package Inst_1 is new Gen_Pack;                                   --  OK
   package Inst_2 is new Gen_Pack with Part_Of => Pack_State;        --  OK
end Pack;

--  pack.adb

package body Pack
  with Refined_State => (Pack_State => Inst_2.Val)
is
   procedure Force_Body is null;
end Pack;

-----------------
-- Compilation --
-----------------

$ gcc -c pack.adb

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

gcc/ada/

	* sem_prag.adb (Has_Visible_State): Do not consider constants as
	visible state because it is not possible to determine whether a
	constant depends on variable input.
	(Propagate_Part_Of): Add comment clarifying the behavior with respect
	to constant.

From-SVN: r262782

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0dbbe8c..c98f8d3 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,11 @@
+2018-07-17  Hristian Kirtchev  <kirtchev@adacore.com>
+
+       * sem_prag.adb (Has_Visible_State): Do not consider constants as
+       visible state because it is not possible to determine whether a
+       constant depends on variable input.
+       (Propagate_Part_Of): Add comment clarifying the behavior with respect
+       to constant.
+
 2018-07-17  Yannick Moy  <moy@adacore.com>
 
        * gnat1drv.adb (Gnat1drv): Do not issue warning about exception not

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 37b7d23..babae30 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -19991,6 +19991,9 @@ package body Sem_Prag is
 
                      --  The Part_Of indicator turns an abstract state or an
                      --  object into a constituent of the encapsulating state.
+                     --  Note that constants are considered here even though
+                     --  they may not depend on variable input. This check is
+                     --  left to the SPARK prover.
 
                      elsif Ekind_In (Item_Id, E_Abstract_State,
                                               E_Constant,
@@ -28789,12 +28792,12 @@ package body Sem_Prag is
             elsif Is_Hidden (Item_Id) then
                null;
 
-            --  A visible state has been found
+            --  A visible state has been found. Note that constants are not
+            --  considered here because it is not possible to determine whether
+            --  they depend on variable input. This check is left to the SPARK
+            --  prover.
 
-            elsif Ekind_In (Item_Id, E_Abstract_State,
-                                     E_Constant,
-                                     E_Variable)
-            then
+            elsif Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
                return True;
 
             --  Recursively peek into nested packages and instantiations