[Ada] Spurious error on Part_Of indicator

Message ID 20180717082342.GA1392@adacore.com
State New
Headers show
Series
  • [Ada] Spurious error on Part_Of indicator
Related show

Commit Message

Pierre-Marie de Rodat July 17, 2018, 8:23 a.m.
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

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

Patch

--- gcc/ada/sem_prag.adb
+++ 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