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 <kirtc...@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.--- 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
