SPARK RM 7.2.6(5) allows the hidden state of a generic package to be Part_Of
the state of the generic package. This was not properly supported. Now fixed.
The following code compiles without errors.
$ gcc -c gen.ads
1. generic
2. J : Integer;
3. package Gen with
4. SPARK_Mode => On,
5. Abstract_State => State
6. is
7. G : Boolean;
8. private
9. H : Boolean with Part_Of => State;
10. end Gen;
Tested on x86_64-pc-linux-gnu, committed on trunk
2017-09-18 Yannick Moy <m...@adacore.com>
* sem_util.adb (Find_Placement_In_State_Space): Allow generic package
holding state.
Index: sem_util.adb
===================================================================
--- sem_util.adb (revision 252907)
+++ sem_util.adb (working copy)
@@ -7922,7 +7922,7 @@
Context := Scope (Item_Id);
while Present (Context) and then Context /= Standard_Standard loop
- if Ekind (Context) = E_Package then
+ if Is_Package_Or_Generic_Package (Context) then
Pack_Id := Context;
-- A package body is a cut off point for the traversal as the item
