This is the mail archive of the
gcc-cvs@gcc.gnu.org
mailing list for the GCC project.
r262782 - in /trunk/gcc/ada: ChangeLog sem_prag...
- From: pmderodat at gcc dot gnu dot org
- To: gcc-cvs at gcc dot gnu dot org
- Date: Tue, 17 Jul 2018 08:07:37 -0000
- Subject: r262782 - in /trunk/gcc/ada: ChangeLog sem_prag...
Author: pmderodat
Date: Tue Jul 17 08:07:37 2018
New Revision: 262782
URL: https://gcc.gnu.org/viewcvs?rev=262782&root=gcc&view=rev
Log:
[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.
Modified:
trunk/gcc/ada/ChangeLog
trunk/gcc/ada/sem_prag.adb