@@ -1139,6 +1139,17 @@ package body Sem_Prag is
(State_Id => Item_Id,
Ref => Item);
end if;
+
+ elsif Ekind (Item_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Item_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Depends",
+ Item, Item_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Item, Ultimate_Overlaid_Entity (Item_Id));
+ return;
end if;
-- When the item renames an entire object, replace the
@@ -2387,6 +2398,17 @@ package body Sem_Prag is
elsif Is_Formal_Object (Item_Id) then
null;
+ elsif Ekind (Item_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Item_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Global",
+ Item, Item_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Item, Ultimate_Overlaid_Entity (Item_Id));
+ return;
+
-- The only legal references are those to abstract states,
-- objects and various kinds of constants (SPARK RM 6.1.4(4)).
@@ -2984,6 +3006,16 @@ package body Sem_Prag is
if Item_Id = Any_Id then
null;
+ elsif Ekind (Item_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Item_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Initializes",
+ Item, Item_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Item, Ultimate_Overlaid_Entity (Item_Id));
+
-- The state or variable must be declared in the visible
-- declarations of the package (SPARK RM 7.1.5(7)).
@@ -3126,6 +3158,18 @@ package body Sem_Prag is
end if;
end if;
+ if Ekind (Input_Id) in E_Constant | E_Variable
+ and then Present (Ultimate_Overlaid_Entity (Input_Id))
+ then
+ SPARK_Msg_NE
+ ("overlaying object & cannot appear in Initializes",
+ Input, Input_Id);
+ SPARK_Msg_NE
+ ("\use the overlaid object & instead",
+ Input, Ultimate_Overlaid_Entity (Input_Id));
+ return;
+ end if;
+
-- Detect a duplicate use of the same input item
-- (SPARK RM 7.1.5(5)).
@@ -5708,6 +5708,13 @@ package body Sem_Util is
if Ekind (State_Id) = E_Constant then
null;
+ -- Overlays do not contribute to package state
+
+ elsif Ekind (State_Id) = E_Variable
+ and then Present (Ultimate_Overlaid_Entity (State_Id))
+ then
+ null;
+
-- Generate an error message of the form:
-- body of package ... has unused hidden states
@@ -29312,6 +29319,39 @@ package body Sem_Util is
end if;
end Type_Without_Stream_Operation;
+ ------------------------------
+ -- Ultimate_Overlaid_Entity --
+ ------------------------------
+
+ function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id is
+ Address : Node_Id;
+ Alias : Entity_Id := E;
+ Offset : Boolean;
+
+ begin
+ -- Currently this routine is only called for stand-alone objects that
+ -- have been analysed, since the analysis of the Address aspect is often
+ -- delayed.
+
+ pragma Assert (Ekind (E) in E_Constant | E_Variable);
+
+ loop
+ Address := Address_Clause (Alias);
+ if Present (Address) then
+ Find_Overlaid_Entity (Address, Alias, Offset);
+ if Present (Alias) then
+ null;
+ else
+ return Empty;
+ end if;
+ elsif Alias = E then
+ return Empty;
+ else
+ return Alias;
+ end if;
+ end loop;
+ end Ultimate_Overlaid_Entity;
+
---------------------
-- Ultimate_Prefix --
---------------------
@@ -3275,6 +3275,15 @@ package Sem_Util is
-- prevents the construction of a composite stream operation. If Op is
-- specified we check only for the given stream operation.
+ function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id;
+ -- If entity E is overlaying some other entity via an Address clause (which
+ -- possibly overlays yet another entity via its own Address clause), then
+ -- return the ultimate overlaid entity. If entity E is not overlaying any
+ -- other entity (or the overlaid entity cannot be determined statically),
+ -- then return Empty.
+ --
+ -- Subsidiary to the analysis of object overlays in SPARK.
+
function Ultimate_Prefix (N : Node_Id) return Node_Id;
-- Obtain the "outermost" prefix of arbitrary node N. Return N if no such
-- prefix exists.