2013-10-17 Vincent Celier <celier@adacore.com>

	* gnat_ugn.texi: Remove VMS conversion of -gnatet and -gnateT,
	now that they are both in ug_words.
	* ug_words: Update qualifier for -gnatet Add qualifier for -gnateT
	* vms_data.ads: Update qualifier for -gnatet Add qualifier
	for -gnateT
	* projects.texi: Continue to update the project documentation
	for VMS.

2013-10-17  Robert Dewar  <dewar@adacore.com>

	* einfo.ads, einfo.adb (Has_Body_References): New flag.
	(Body_References): New field.
	* sem_prag.adb (Record_Possible_Body_Reference): New procedure
	(Analyze_Input_Output): Call Record_Possible_Body_Reference
	(Analyze_Global_Item): Call Record_Possible_Body_Reference
	(Analyze_Refinement_Clause): Output messages if illegal global refs.

2013-10-17  Thomas Quinot  <quinot@adacore.com>

	* freeze.adb (Check_Component_Storage_Order): Reject a record or
	array type that does not have an explicit Scalar_Storage_Order
	attribute definition if a component of the record, or the
	elements of the array, have one.
	* gnat_rm.texi (attribute Scalar_Storage_Order): Document the above
	rule.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@203750 138bc75d-0d04-0410-961f-82ee72b054a4

10 files changed, 215 insertions, 49 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e6cfe6d0b42..ce029b4a8d1 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,33 @@
 2013-10-17  Vincent Celier  <celier@adacore.com>
 
+	* gnat_ugn.texi: Remove VMS conversion of -gnatet and -gnateT,
+	now that they are both in ug_words.
+	* ug_words: Update qualifier for -gnatet Add qualifier for -gnateT
+	* vms_data.ads: Update qualifier for -gnatet Add qualifier
+	for -gnateT
+	* projects.texi: Continue to update the project documentation
+	for VMS.
+
+2013-10-17  Robert Dewar  <dewar@adacore.com>
+
+	* einfo.ads, einfo.adb (Has_Body_References): New flag.
+	(Body_References): New field.
+	* sem_prag.adb (Record_Possible_Body_Reference): New procedure
+	(Analyze_Input_Output): Call Record_Possible_Body_Reference
+	(Analyze_Global_Item): Call Record_Possible_Body_Reference
+	(Analyze_Refinement_Clause): Output messages if illegal global refs.
+
+2013-10-17  Thomas Quinot  <quinot@adacore.com>
+
+	* freeze.adb (Check_Component_Storage_Order): Reject a record or
+	array type that does not have an explicit Scalar_Storage_Order
+	attribute definition if a component of the record, or the
+	elements of the array, have one.
+	* gnat_rm.texi (attribute Scalar_Storage_Order): Document the above
+	rule.
+
+2013-10-17  Vincent Celier  <celier@adacore.com>
+
 	* gnat_ugn.texi: Add examples of switches -gnateD, including
 	one where the value is a string.
 	* projects.texi: Do not convert switches in project files to
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 8636d8511cd..5047ec257ce 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -132,6 +132,7 @@ package body Einfo is
    --    String_Literal_Low_Bound        Node15
 
    --    Access_Disp_Table               Elist16
+   --    Body_References                 Elist16
    --    Cloned_Subtype                  Node16
    --    DTC_Entity                      Node16
    --    Entry_Formal                    Node16
@@ -552,8 +553,8 @@ package body Einfo is
    --    Has_Delayed_Rep_Aspects         Flag261
    --    May_Inherit_Delayed_Rep_Aspects Flag262
    --    Has_Visible_Refinement          Flag263
+   --    Has_Body_References             Flag264
 
-   --    (unused)                        Flag264
    --    (unused)                        Flag265
    --    (unused)                        Flag266
    --    (unused)                        Flag267
@@ -733,6 +734,12 @@ package body Einfo is
       return Flag40 (Id);
    end Body_Needed_For_SAL;
 
+   function Body_References (Id : E) return L is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      return Elist16 (Id);
+   end Body_References;
+
    function C_Pass_By_Copy (Id : E) return B is
    begin
       pragma Assert (Is_Record_Type (Id));
@@ -1294,6 +1301,12 @@ package body Einfo is
       return Flag139 (Id);
    end Has_Biased_Representation;
 
+   function Has_Body_References (Id : E) return B is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      return Flag264 (Id);
+   end Has_Body_References;
+
    function Has_Completion (Id : E) return B is
    begin
       return Flag26 (Id);
@@ -3336,6 +3349,12 @@ package body Einfo is
       Set_Flag40 (Id, V);
    end Set_Body_Needed_For_SAL;
 
+   procedure Set_Body_References (Id : E; V : L) is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Set_Elist16 (Id, V);
+   end Set_Body_References;
+
    procedure Set_C_Pass_By_Copy (Id : E; V : B := True) is
    begin
       pragma Assert (Is_Record_Type (Id) and then Is_Base_Type (Id));
@@ -3909,6 +3928,12 @@ package body Einfo is
       Set_Flag139 (Id, V);
    end Set_Has_Biased_Representation;
 
+   procedure Set_Has_Body_References (Id : E; V : B := True) is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Set_Flag264 (Id, V);
+   end Set_Has_Body_References;
+
    procedure Set_Has_Completion (Id : E; V : B := True) is
    begin
       Set_Flag26 (Id, V);
@@ -7984,6 +8009,7 @@ package body Einfo is
       W ("Has_Anonymous_Master",            Flag253 (Id));
       W ("Has_Atomic_Components",           Flag86  (Id));
       W ("Has_Biased_Representation",       Flag139 (Id));
+      W ("Has_Body_References",             Flag264 (Id));
       W ("Has_Completion",                  Flag26  (Id));
       W ("Has_Completion_In_Body",          Flag71  (Id));
       W ("Has_Complex_Representation",      Flag140 (Id));
@@ -8672,6 +8698,10 @@ package body Einfo is
    procedure Write_Field16_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+
+         when E_Abstract_State                             =>
+            Write_Str ("Body_References");
+
          when E_Record_Type                                |
               E_Record_Type_With_Private                   =>
             Write_Str ("Access_Disp_Table");
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 0526d4406e8..6520fe6bdad 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -493,6 +493,12 @@ package Einfo is
 --       units. Indicates that the source for the body must be included
 --       when the unit is part of a standalone library.
 
+--    Body_References (Elist16)
+--       Defined in abstract state entities. Only set if Has_Body_References
+--       flag is set True, in which case it contains an element list of global
+--       references (identifiers) in the current package body to this abstract
+--       state that are illegal if the abstract state has a visible refinement.
+
 --    C_Pass_By_Copy (Flag125) [implementation base type only]
 --       Defined in record types. Set if a pragma Convention for the record
 --       type specifies convention C_Pass_By_Copy. This convention name is
@@ -1405,6 +1411,10 @@ package Einfo is
 --       size of the type, forcing biased representation for the object, but
 --       the subtype is still an unbiased type.
 
+--    Has_Body_References (Flag264)
+--       Defined in entities for abstract states. Set if Body_References has
+--       at least one entry.
+
 --    Has_Completion (Flag26)
 --       Defined in all entities that require a completion (functions,
 --       procedures, private types, limited private types, incomplete types,
@@ -5117,6 +5127,8 @@ package Einfo is
    --  E_Abstract_State
    --    Refinement_Constituents             (Elist8)
    --    Refined_State                       (Node10)
+   --    Body_References                     (Elist16)
+   --    Has_Body_References                 (Flag264)
    --    Has_Visible_Refinement              (Flag263)
    --    Has_Non_Null_Refinement             (synth)
    --    Has_Null_Refinement                 (synth)
@@ -6230,6 +6242,7 @@ package Einfo is
    function Block_Node                          (Id : E) return N;
    function Body_Entity                         (Id : E) return E;
    function Body_Needed_For_SAL                 (Id : E) return B;
+   function Body_References                     (Id : E) return L;
    function CR_Discriminant                     (Id : E) return E;
    function C_Pass_By_Copy                      (Id : E) return B;
    function Can_Never_Be_Null                   (Id : E) return B;
@@ -6325,6 +6338,7 @@ package Einfo is
    function Has_Anonymous_Master                (Id : E) return B;
    function Has_Atomic_Components               (Id : E) return B;
    function Has_Biased_Representation           (Id : E) return B;
+   function Has_Body_References                 (Id : E) return B;
    function Has_Completion                      (Id : E) return B;
    function Has_Completion_In_Body              (Id : E) return B;
    function Has_Complex_Representation          (Id : E) return B;
@@ -6848,6 +6862,7 @@ package Einfo is
    procedure Set_Block_Node                      (Id : E; V : N);
    procedure Set_Body_Entity                     (Id : E; V : E);
    procedure Set_Body_Needed_For_SAL             (Id : E; V : B := True);
+   procedure Set_Body_References                 (Id : E; V : L);
    procedure Set_CR_Discriminant                 (Id : E; V : E);
    procedure Set_C_Pass_By_Copy                  (Id : E; V : B := True);
    procedure Set_Can_Never_Be_Null               (Id : E; V : B := True);
@@ -6942,6 +6957,7 @@ package Einfo is
    procedure Set_Has_Anonymous_Master            (Id : E; V : B := True);
    procedure Set_Has_Atomic_Components           (Id : E; V : B := True);
    procedure Set_Has_Biased_Representation       (Id : E; V : B := True);
+   procedure Set_Has_Body_References             (Id : E; V : B := True);
    procedure Set_Has_Completion                  (Id : E; V : B := True);
    procedure Set_Has_Completion_In_Body          (Id : E; V : B := True);
    procedure Set_Has_Complex_Representation      (Id : E; V : B := True);
@@ -7568,6 +7584,7 @@ package Einfo is
    pragma Inline (Block_Node);
    pragma Inline (Body_Entity);
    pragma Inline (Body_Needed_For_SAL);
+   pragma Inline (Body_References);
    pragma Inline (CR_Discriminant);
    pragma Inline (C_Pass_By_Copy);
    pragma Inline (Can_Never_Be_Null);
@@ -7660,6 +7677,7 @@ package Einfo is
    pragma Inline (Has_Anonymous_Master);
    pragma Inline (Has_Atomic_Components);
    pragma Inline (Has_Biased_Representation);
+   pragma Inline (Has_Body_References);
    pragma Inline (Has_Completion);
    pragma Inline (Has_Completion_In_Body);
    pragma Inline (Has_Complex_Representation);
@@ -8031,6 +8049,7 @@ package Einfo is
    pragma Inline (Set_Block_Node);
    pragma Inline (Set_Body_Entity);
    pragma Inline (Set_Body_Needed_For_SAL);
+   pragma Inline (Set_Body_References);
    pragma Inline (Set_CR_Discriminant);
    pragma Inline (Set_C_Pass_By_Copy);
    pragma Inline (Set_Can_Never_Be_Null);
@@ -8121,6 +8140,7 @@ package Einfo is
    pragma Inline (Set_Has_Anonymous_Master);
    pragma Inline (Set_Has_Atomic_Components);
    pragma Inline (Set_Has_Biased_Representation);
+   pragma Inline (Set_Has_Body_References);
    pragma Inline (Set_Has_Completion);
    pragma Inline (Set_Has_Completion_In_Body);
    pragma Inline (Set_Has_Complex_Representation);
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index d07944ae05f..1ab8f1e7bda 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -92,11 +92,15 @@ package body Freeze is
 
    procedure Check_Component_Storage_Order
      (Encl_Type : Entity_Id;
-      Comp      : Entity_Id);
+      Comp      : Entity_Id;
+      ADC       : Node_Id);
    --  For an Encl_Type that has a Scalar_Storage_Order attribute definition
-   --  clause, verify that the component type is compatible. For arrays,
-   --  Comp is Empty; for records, it is the entity of the component under
-   --  consideration.
+   --  clause, verify that the component type has an explicit and compatible
+   --  attribute/aspect. For arrays, Comp is Empty; for records, it is the
+   --  entity of the component under consideration. For an Encl_Type that
+   --  does not have a Scalar_Storage_Order attribute definition clause,
+   --  verify that the component also does not have such a clause.
+   --  ADC is the attribute definition clause if present (or Empty).
 
    procedure Check_Strict_Alignment (E : Entity_Id);
    --  E is a base type. If E is tagged or has a component that is aliased
@@ -1068,11 +1072,12 @@ package body Freeze is
 
    procedure Check_Component_Storage_Order
      (Encl_Type : Entity_Id;
-      Comp      : Entity_Id)
+      Comp      : Entity_Id;
+      ADC       : Node_Id)
    is
       Comp_Type : Entity_Id;
+      Comp_ADC  : Node_Id;
       Err_Node  : Node_Id;
-      ADC       : Node_Id;
 
       Comp_Byte_Aligned : Boolean;
       --  Set True for the record case, when Comp starts on a byte boundary
@@ -1113,11 +1118,24 @@ package body Freeze is
       --  the attribute definition clause is attached to the first subtype.
 
       Comp_Type := Base_Type (Comp_Type);
-      ADC := Get_Attribute_Definition_Clause
-               (First_Subtype (Comp_Type),
-                Attribute_Scalar_Storage_Order);
+      Comp_ADC := Get_Attribute_Definition_Clause
+                    (First_Subtype (Comp_Type),
+                     Attribute_Scalar_Storage_Order);
 
-      if Is_Record_Type (Comp_Type) or else Is_Array_Type (Comp_Type) then
+      --  Case of enclosing type not having explicit SSO: component cannot
+      --  have it either.
+
+      if No (ADC) then
+         if Present (Comp_ADC) then
+            Error_Msg_N
+              ("composite type must have explicit scalar storage order",
+               Err_Node);
+         end if;
+
+      --  Case of enclosing type having explicit SSO: check compatible
+      --  attribute on Comp_Type if composite.
+
+      elsif Is_Record_Type (Comp_Type) or else Is_Array_Type (Comp_Type) then
          if Present (Comp) and then Chars (Comp) = Name_uParent then
             if Reverse_Storage_Order (Encl_Type)
                  /=
@@ -1142,6 +1160,9 @@ package body Freeze is
                & "storage order as enclosing composite", Err_Node);
          end if;
 
+      --  Enclosing type has explicit SSO, non-composite component must not
+      --  be aliased.
+
       elsif Component_Aliased then
          Error_Msg_N
            ("aliased component not permitted for type with "
@@ -2312,11 +2333,12 @@ package body Freeze is
 
             --  Check for scalar storage order
 
-            if Present (Get_Attribute_Definition_Clause
-                        (Arr, Attribute_Scalar_Storage_Order))
-            then
-               Check_Component_Storage_Order (Arr, Empty);
-            end if;
+            Check_Component_Storage_Order
+              (Encl_Type => Arr,
+               Comp      => Empty,
+               ADC       => Get_Attribute_Definition_Clause
+                              (First_Subtype (Arr),
+                               Attribute_Scalar_Storage_Order));
 
             --  Processing that is done only for subtypes
 
@@ -2999,15 +3021,16 @@ package body Freeze is
                  ("??scalar storage order specified but no component clause",
                   ADC);
             end if;
+         end if;
 
-            --  Check attribute on component types
+         --  Check consistent attribute setting on component types
 
-            Comp := First_Component (Rec);
-            while Present (Comp) loop
-               Check_Component_Storage_Order (Rec, Comp);
-               Next_Component (Comp);
-            end loop;
-         end if;
+         Comp := First_Component (Rec);
+         while Present (Comp) loop
+            Check_Component_Storage_Order
+              (Encl_Type => Rec, Comp => Comp, ADC => ADC);
+            Next_Component (Comp);
+         end loop;
 
          --  Deal with Bit_Order aspect specifying a non-default bit order
 
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index ff8013be9d5..5dcfbe86634 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -8727,6 +8727,10 @@ have a @code{Scalar_Storage_Order} attribute definition clause. In addition,
 if the component does not start on a byte boundary, then the scalar storage
 order specified for S and for the nested component type shall be identical.
 
+If @var{S} appears as the type of a record or array component, the enclosing
+record or array shall also have a @code{Scalar_Storage_Order} attribute
+definition clause.
+
 No component of a type that has a @code{Scalar_Storage_Order} attribute
 definition may be aliased.
 
diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi
index b737b326645..4b103039759 100644
--- a/gcc/ada/gnat_ugn.texi
+++ b/gcc/ada/gnat_ugn.texi
@@ -3825,12 +3825,12 @@ temporary use of special test software.
 @cindex @option{-gnateS} (@command{gcc})
 Synonym of @option{-fdump-scos}, kept for backards compatibility.
 
-@item ^-gnatet^/TARGET_DEPENDENT_INFO^=@var{path}
+@item -gnatet=@var{path}
 @cindex @option{-gnatet=file} (@command{gcc})
 Generate target dependent information. The format of the output file is
 described in the section about switch @option{-gnateT}.
 
-@item ^-gnateT^/TARGET_DEPENDENT_INFO^=@var{path}
+@item -gnateT=@var{path}
 @cindex @option{-gnateT} (@command{gcc})
 Read target dependent information, such as endianness or sizes and alignments
 of base type. If this switch is passed, the default target dependent
diff --git a/gcc/ada/projects.texi b/gcc/ada/projects.texi
index 01a02937fbe..166a9e829c0 100644
--- a/gcc/ada/projects.texi
+++ b/gcc/ada/projects.texi
@@ -3170,10 +3170,10 @@ The following packages are currently supported in project files
   @command{gnatfind} via the @command{gnat} driver. Its attributes
   @b{Default_Switches} and @b{^Switches^Switches^} have the same semantics as for the
   package @code{Builder}.
-@item Gnatls
+@item ^Gnatls^Gnatls^
   This package the options to use when invoking @command{gnatls} via the
   @command{gnat} driver.
-@item Gnatstub
+@item ^Gnatstub^Gnatstub^
   This package specifies the options used when calling the tool
   @command{gnatstub} via the @command{gnat} driver. Its attributes
   @b{Default_Switches} and @b{^Switches^Switches^} have the same semantics as for the
@@ -3630,8 +3630,8 @@ end MyProj;
 * Package Cross_Reference Attributes::
 * Package Eliminate Attributes::
 * Package Finder Attributes::
-* Package gnatls Attributes::
-* Package gnatstub Attributes::
+* Package ^gnatls^gnatls^ Attributes::
+* Package ^gnatstub^gnatstub^ Attributes::
 * Package IDE Attributes::
 * Package Install Attributes::
 * Package Linker Attributes::
@@ -4630,8 +4630,8 @@ invoking @code{gnatfind} for the source.
 
 @end itemize
 
-@node Package gnatls Attributes
-@subsubsection Package gnatls Attributes
+@node Package ^gnatls^gnatls^ Attributes
+@subsubsection Package ^gnatls^gnatls^ Attributes
 
 @itemize @bullet
 
@@ -4641,8 +4641,8 @@ Value is a list of switches to be used when invoking @code{gnatls}.
 
 @end itemize
 
-@node Package gnatstub Attributes
-@subsubsection Package gnatstub Attributes
+@node Package ^gnatstub^gnatstub^ Attributes
+@subsubsection Package ^gnatstub^gnatstub^ Attributes
 
 @itemize @bullet
 
@@ -4650,7 +4650,7 @@ Value is a list of switches to be used when invoking @code{gnatls}.
 
 Index is a language name. Value is a list of switches to be used when invoking
 @code{gnatstub} for a source of the language, if there is no applicable
-attribute Switches.
+attribute ^Switches^Switches^.
 
 @item @b{^Switches^Switches^}: list, optional index, indexed, case-insensitive index,
                     others allowed
@@ -4699,11 +4699,11 @@ the handling of switches.
 Value is a string that specifies the name of the debugger to be used, such as
 gdb, powerpc-wrs-vxworks-gdb or gdb-4.
 
-@item @b{gnatlist}: single
+@item @b{^gnatlist^gnatlist^}: single
 
-Value is a string that specifies the name of the @command{gnatls} utility
+Value is a string that specifies the name of the @command{^gnatls^gnatls^} utility
 to be used to retrieve information about the predefined path; for example,
-@code{"gnatls"}, @code{"powerpc-wrs-vxworks-gnatls"}.
+@code{"^gnatls^gnatls^"}, @code{"powerpc-wrs-vxworks-gnatls"}.
 
 @item @b{VCS_Kind}: single
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 34b9d973579..0b758a2591d 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -277,23 +277,30 @@ package body Sem_Prag is
    --  of a Test_Case pragma if present (possibly Empty). We treat these as
    --  spec expressions (i.e. similar to a default expression).
 
+   procedure Record_Possible_Body_Reference
+     (Item    : Node_Id;
+      Item_Id : Entity_Id);
+   --  Given an entity reference (Item) and the corresponding Entity (Item_Id),
+   --  determines if we have a body reference to an abstract state, which may
+   --  be illegal if the state is refined within the body.
+
    procedure Rewrite_Assertion_Kind (N : Node_Id);
    --  If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
    --  then it is rewritten as an identifier with the corresponding special
    --  name _Pre, _Post, _Invariant, or _Type_Invariant. Used by pragmas
    --  Check, Check_Policy.
 
+   procedure Set_Unit_Name (N : Node_Id; With_Item : Node_Id);
+   --  Place semantic information on the argument of an Elaborate/Elaborate_All
+   --  pragma. Entity name for unit and its parents is taken from item in
+   --  previous with_clause that mentions the unit.
+
    procedure rv;
    --  This is a dummy function called by the processing for pragma Reviewable.
    --  It is there for assisting front end debugging. By placing a Reviewable
    --  pragma in the source program, a breakpoint on rv catches this place in
    --  the source, allowing convenient stepping to the point of interest.
 
-   procedure Set_Unit_Name (N : Node_Id; With_Item : Node_Id);
-   --  Place semantic information on the argument of an Elaborate/Elaborate_All
-   --  pragma. Entity name for unit and its parents is taken from item in
-   --  previous with_clause that mentions the unit.
-
    --------------
    -- Add_Item --
    --------------
@@ -772,6 +779,8 @@ package body Sem_Prag is
 
                Item_Id := Entity_Of (Item);
 
+               Record_Possible_Body_Reference (Item, Item_Id);
+
                if Present (Item_Id) then
                   if Ekind_In (Item_Id, E_Abstract_State,
                                         E_In_Parameter,
@@ -1645,6 +1654,7 @@ package body Sem_Prag is
             Item_Id := Entity_Of (Item);
 
             if Present (Item_Id) then
+               Record_Possible_Body_Reference (Item, Item_Id);
 
                --  A global item may denote a formal parameter of an enclosing
                --  subprogram. Do this check first to provide a better error
@@ -21641,6 +21651,29 @@ package body Sem_Prag is
                        ("& must denote an abstract state", State, State_Id);
                   end if;
 
+                  --  Enforce SPARK RM (6.1.5(4)): A global item shall not
+                  --  denote a state abstraction whose refinement is visible
+                  --  (a state abstraction cannot be named within its enclosing
+                  --  package's body other than in its refinement).
+
+                  if Has_Body_References (State_Id) then
+                     declare
+                        Ref : Elmt_Id;
+                        Nod : Node_Id;
+                     begin
+                        Ref := First_Elmt (Body_References (State_Id));
+                        while Present (Ref) loop
+                           Nod := Node (Ref);
+                           Error_Msg_N
+                             ("global reference to & not allowed "
+                              & "(SPARK RM 6.1.5(4))", Nod);
+                           Error_Msg_Sloc := Sloc (State);
+                           Error_Msg_N ("\refinement of & is visible#", Nod);
+                           Next_Elmt (Ref);
+                        end loop;
+                     end;
+                  end if;
+
                --  The state name is illegal
 
                else
@@ -23296,6 +23329,27 @@ package body Sem_Prag is
 
    end Process_Compilation_Unit_Pragmas;
 
+   ------------------------------------
+   -- Record_Possible_Body_Reference --
+   ------------------------------------
+
+   procedure Record_Possible_Body_Reference
+     (Item    : Node_Id;
+      Item_Id : Entity_Id)
+   is
+   begin
+      if In_Package_Body
+        and then Ekind (Item_Id) = E_Abstract_State
+      then
+         if not Has_Body_References (Item_Id) then
+            Set_Has_Body_References (Item_Id, True);
+            Set_Body_References (Item_Id, New_Elmt_List);
+         end if;
+
+         Append_Elmt (Item, Body_References (Item_Id));
+      end if;
+   end Record_Possible_Body_Reference;
+
    ------------------------------
    -- Relocate_Pragmas_To_Body --
    ------------------------------
diff --git a/gcc/ada/ug_words b/gcc/ada/ug_words
index 48999791e62..bae43b97edd 100644
--- a/gcc/ada/ug_words
+++ b/gcc/ada/ug_words
@@ -72,7 +72,8 @@ gcc -c          ^ GNAT COMPILE
 -gnatep         ^ /DATA_PREPROCESSING
 -gnateP         ^ /CATEGORIZATION_WARNINGS
 -gnateS         ^ /SCO_OUTPUT
--gnatet         ^ /TARGET_DEPENDENT_INFO
+-gnatet         ^ /WRITE_TARGET_DEPENDENT_INFO
+-gnateT         ^ /READ_TARGET_DEPENDENT_INFO
 -gnateV         ^ /PARAMETER_VALIDITY_CHECK
 -gnateY         ^ /IGNORE_STYLE_CHECKS_PRAGMAS
 -gnatE          ^ /CHECKS=ELABORATION
diff --git a/gcc/ada/vms_data.ads b/gcc/ada/vms_data.ads
index 7b0fd2c95ec..6fc9ed0886b 100644
--- a/gcc/ada/vms_data.ads
+++ b/gcc/ada/vms_data.ads
@@ -2885,12 +2885,17 @@ package VMS_Data is
    --
    --   All compiler tables start at nnn times usual starting size.
 
-   S_GCC_Target  : aliased constant S := "/TARGET_DEPENDENT_INFO "         &
-                                             "-gnatet";
-   --        /NOTARGET_DEPENDENT_INFO (D)
-   --        /TARGET_DEPENDENT_INFO
+   S_GCC_Target_W  : aliased constant S := "/WRITE_TARGET_DEPENDENT_INFO=<" &
+                                             "-gnatet=>";
+   --        /WRITE_TARGET_DEPENDENT_INFO=file
    --
-   --   Generate target dependent information.
+   --   Generate target dependent information to file.
+
+   S_GCC_Target_R  : aliased constant S := "/READ_TARGET_DEPENDENT_INFO=<"  &
+                                             "-gnateT=>";
+   --        /READ_TARGET_DEPENDENT_INFO=file
+   --
+   --   Read target dependent information from file.
 
    S_GCC_Trace   : aliased constant S := "/TRACE_UNITS "                   &
                                             "-gnatdc";
@@ -3743,7 +3748,8 @@ package VMS_Data is
                      S_GCC_Symbol  'Access,
                      S_GCC_Syntax  'Access,
                      S_GCC_Table   'Access,
-                     S_GCC_Target  'Access,
+                     S_GCC_Target_W'Access,
+                     S_GCC_Target_R'Access,
                      S_GCC_Trace   'Access,
                      S_GCC_Tree    'Access,
                      S_GCC_Trys    'Access,