From e6bc029a34598dd3af5c6a0aacd66ee62235cdfe Mon Sep 17 00:00:00 2001 From: Hristian Kirtchev Date: Tue, 17 Jul 2018 08:07:37 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 8 ++++++++ gcc/ada/sem_prag.adb | 13 ++++++++----- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0dbbe8c..c98f8d3 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2018-07-17 Hristian Kirtchev + + * 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 * 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 37b7d23..babae30 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 -- 2.7.4