[Ada] Reject overlays in Global/Depends/Initializes contracts

gcc/ada/

	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Reject overlays
	in Depends and Refined_Depends contracts.
	(Analyze_Global_In_Decl_Part): Likewise for Global and
	Refined_Global.
	(Analyze_Initializes_In_Decl_Part): Likewise for Initializes
	(when appearing both as a single item and as a initialization
	clause).
	* sem_util.ads (Ultimate_Overlaid_Entity): New routine.
	* sem_util.adb (Report_Unused_Body_States): Ignore overlays.
	(Ultimate_Overlaid_Entity): New routine.

3 files changed, 93 insertions, 0 deletions

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0efdcef..41e887d 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -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)).
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 7ea809b..038c1ee 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -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 --
    ---------------------
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index a49272e..7cacae2 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -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.