diff options
| author | Hristian Kirtchev <kirtchev@adacore.com> | 2018-07-17 08:07:37 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2018-07-17 08:07:37 +0000 |
| commit | e6bc029a34598dd3af5c6a0aacd66ee62235cdfe (patch) | |
| tree | 419525e839b5e749c0c7066c2f022a0daa290b8f | |
| parent | 014eddc6d9cec9d0fd526b1e2d3d9cb4f0674f63 (diff) | |
| download | gcc-e6bc029a34598dd3af5c6a0aacd66ee62235cdfe.zip gcc-e6bc029a34598dd3af5c6a0aacd66ee62235cdfe.tar.gz gcc-e6bc029a34598dd3af5c6a0aacd66ee62235cdfe.tar.bz2 | |
[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.
From-SVN: r262782
| -rw-r--r-- | gcc/ada/ChangeLog | 8 | ||||
| -rw-r--r-- | 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 <kirtchev@adacore.com> + + * 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 <moy@adacore.com> * 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 |