From: Hristian Kirtchev <kirtchev@adacore.com>
Date: Tue, 17 Jul 2018 08:07:37 +0000 (+0000)
Subject: [Ada] Spurious error on Part_Of indicator
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6bc029a34598dd3af5c6a0aacd66ee62235cdfe;p=gcc.git

[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 0dbbe8c11ea..c98f8d31b8e 100644
--- 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 37b7d23d348..babae30bd60 100644
--- 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