ada: Fix Ultimate_Overlaid_Entity to match the SPARK RM semantics

The Ultimate_Overlaid_Entity function should return the root of the
last precisely supported address clause as per the definition in the
SPARK RM.

gcc/ada/ChangeLog:

	* sem_util.ads (Overlaid_Entity): Return the root of the address
	clause of an object if it is precisely supported in SPARK.
	* sem_util.adb (Ultimate_Overlaid_Entity): Use Overlaid_Entity to
	match the SPARK RM semantics.
	* sem_prag.adb (Analyze_Global_Item): Only check for overlays on
	variables.
	(Analyze_Initialization_Item): Likewise.
	(Analyze_Input_Item): Likewise.

diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 0d9f20a714f0f61d4634d8f038635063125a6366..ae98ad6c98f7cb198c56b2b848eacf13af92193a 100644 (file)
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -1361,7 +1361,7 @@ package body Sem_Prag is
                               Ref      => Item);
                         end if;
 
-                     elsif Ekind (Item_Id) in E_Constant | E_Variable
+                     elsif Ekind (Item_Id) = E_Variable
                        and then Present (Ultimate_Overlaid_Entity (Item_Id))
                      then
                         SPARK_Msg_NE
@@ -3286,7 +3286,7 @@ package body Sem_Prag is
                elsif Is_Formal_Object (Item_Id) then
                   null;
 
-               elsif Ekind (Item_Id) in E_Constant | E_Variable
+               elsif Ekind (Item_Id) = E_Variable
                  and then Present (Ultimate_Overlaid_Entity (Item_Id))
                then
                   SPARK_Msg_NE
@@ -3910,7 +3910,7 @@ package body Sem_Prag is
                if Item_Id = Any_Id then
                   null;
 
-               elsif Ekind (Item_Id) in E_Constant | E_Variable
+               elsif Ekind (Item_Id) = E_Variable
                  and then Present (Ultimate_Overlaid_Entity (Item_Id))
                then
                   SPARK_Msg_NE
@@ -4062,7 +4062,7 @@ package body Sem_Prag is
                         end if;
                      end if;
 
-                     if Ekind (Input_Id) in E_Constant | E_Variable
+                     if Ekind (Input_Id) = E_Variable
                        and then Present (Ultimate_Overlaid_Entity (Input_Id))
                      then
                         SPARK_Msg_NE

diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index ad7c0e647f09b132b5f8159e3cf955f7215f86d5..dfbe15b5d2a5325ca48f5d45ebdaa910d5590dc9 100644 (file)
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -26639,6 +26639,71 @@ package body Sem_Util is
       Write_Eol;
    end Output_Name;
 
+   ---------------------
+   -- Overlaid_Entity --
+   ---------------------
+
+   function Overlaid_Entity (E : Entity_Id) return Entity_Id is
+      Address : Node_Id;
+
+   begin
+      if Ekind (E) in E_Constant | E_Variable then
+         Address := Address_Clause (E);
+      else
+         return Empty;
+      end if;
+
+      if Present (Address) then
+         declare
+            Expr : Node_Id := Expression (Address);
+
+         begin
+            --  Only support precisely address clauses of the form P'Address
+
+            if Nkind (Expr) = N_Attribute_Reference
+              and then Attribute_Name (Expr) = Name_Address
+            then
+               Expr := Prefix (Expr);
+
+            else
+               return Empty;
+            end if;
+
+            loop
+
+               --  Precisely supported addresses refer to part of objects
+
+               if Is_Entity_Name (Expr) then
+                  if Is_Object (Entity (Expr)) then
+                     return Entity (Expr);
+                  else
+                     return Empty;
+                  end if;
+
+               elsif Nkind (Expr) in N_Selected_Component
+                                   | N_Indexed_Component
+                                   | N_Explicit_Dereference
+               then
+                  Expr := Prefix (Expr);
+
+               --  Taking the address of a slice is only well-defined if the
+               --  components are aliased.
+
+               elsif Nkind (Expr) = N_Slice
+                 and then Has_Aliased_Components (Etype (Etype (Expr)))
+               then
+                  Expr := Prefix (Expr);
+
+               else
+                  return Empty;
+               end if;
+            end loop;
+         end;
+      else
+         return Empty;
+      end if;
+   end Overlaid_Entity;
+
    ------------------
    -- Param_Entity --
    ------------------
@@ -29648,32 +29713,24 @@ package body Sem_Util is
    ------------------------------
 
    function Ultimate_Overlaid_Entity (E : Entity_Id) return Entity_Id is
-      Address  : Node_Id;
-      Alias    : Entity_Id := E;
-      Offset   : Boolean;
-      Ovrl_Typ : Entity_Id;
+      Alias : Entity_Id := E;
 
    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);
+      --  Currently this routine is only called for objects that have been
+      --  analysed, since the analysis of the Address aspect is often delayed.
 
       loop
-         Address := Address_Clause (Alias);
-         if Present (Address) then
-            Find_Overlaid_Entity (Address, Alias, Ovrl_Typ, Offset);
-            if Present (Alias) then
-               null;
-            else
+         declare
+            Address_Root : constant Entity_Id := Overlaid_Entity (Alias);
+         begin
+            if Present (Address_Root) then
+               Alias := Address_Root;
+            elsif Alias = E then
                return Empty;
+            else
+               return Alias;
             end if;
-         elsif Alias = E then
-            return Empty;
-         else
-            return Alias;
-         end if;
+         end;
       end loop;
    end Ultimate_Overlaid_Entity;
 

diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index ab0f305425d73eb62d7aa1df70937fb9515a2b95..146fd10202a5bc480a303efa336985bda68ef591 100644 (file)
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -3431,12 +3431,20 @@ 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 Overlaid_Entity (E : Entity_Id) return Entity_Id;
+   --  This function implements the definition of precisely supported address
+   --  clause in SPARK. If E has an address clause of the form P'Address, where
+   --  P is a part of an object, return the root object of P. Otherwise, return
+   --  Empty.
+   --
+   --  Subsidiary to the analysis of object overlays in SPARK.
+
    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.
+   --  If entity E is overlaying some other entity via a precisely supported
+   --  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.