diff options
author | Yannick Moy <moy@adacore.com> | 2024-01-08 09:53:58 +0100 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2024-05-07 09:55:53 +0200 |
commit | d82909fed0a90a2950e2413429efce655ecba8d2 (patch) | |
tree | 5ad83385f44ef4a7d081938329f30b575714c6f2 | |
parent | 15a8d0dd59dd8c92600a89b6f5fe339e5ce74a11 (diff) | |
download | gcc-d82909fed0a90a2950e2413429efce655ecba8d2.zip gcc-d82909fed0a90a2950e2413429efce655ecba8d2.tar.gz gcc-d82909fed0a90a2950e2413429efce655ecba8d2.tar.bz2 |
ada: Fix spurious error on generic state in SPARK
The public state of a generic package needs not be part of the state of
the enclosing unit, only the state of instantiations need to be accounted
for in the enclosing package. Now fixed.
gcc/ada/
* sem_util.adb (Find_Placement_In_State_Space): Stop search for
placement when reaching the public state of a generic package.
-rw-r--r-- | gcc/ada/sem_util.adb | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 3af029f..d629c76 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -9103,6 +9103,14 @@ package body Sem_Util is Placement := Private_State_Space; return; + -- The item or its enclosing package appear in the visible state + -- space of a generic package. + + elsif Ekind (Pack_Id) = E_Generic_Package then + Placement := Not_In_Package; + Pack_Id := Empty; + return; + -- When the item appears in the visible state space of a package, -- continue to climb the scope stack as this may not be the final -- state space. |