aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2024-01-08 09:53:58 +0100
committerMarc Poulhiès <poulhies@adacore.com>2024-05-07 09:55:53 +0200
commitd82909fed0a90a2950e2413429efce655ecba8d2 (patch)
tree5ad83385f44ef4a7d081938329f30b575714c6f2
parent15a8d0dd59dd8c92600a89b6f5fe339e5ce74a11 (diff)
downloadgcc-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.adb8
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.