[Ada] Spurious error on Part_Of indicator
Pierre-Marie de Rodat
derodat@adacore.com
Tue Jul 17 08:24:00 GMT 2018
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff
Type: text/x-diff
Size: 1379 bytes
Desc: not available
URL: <http://gcc.gnu.org/pipermail/gcc-patches/attachments/20180717/6dbc3798/attachment.bin>
More information about the Gcc-patches
mailing list