2014-01-27 Hristian Kirtchev <kirtchev@adacore.com>

	* einfo.adb (Has_Option): Reimplemented.
	* sem_prag.adb (Analyze_Refinement_Clause): Add global
	variables AR_Constit, AW_Constit, ER_Constit, EW_Constit,
	External_Constit_Seen and State. Add local variables Body_Ref,
	Body_Ref_Elmt and Extra_State. Reimplement part of the logic to
	avoid a cumbersome while pool. Verify the legality of an external
	state and relevant properties.
	(Check_External_Property): New routine.
	(Check_Matching_State): Remove parameter profile
	and update comment on usage.
	(Collect_Constituent): Store the
	relevant external property of a constituent.
	* sem_util.adb (Async_Readers_Enabled): Update the call to
	Has_Enabled_Property.
	(Async_Writers_Enabled): Update the call to Has_Enabled_Property.
	(Effective_Reads_Enabled): Update the call to Has_Enabled_Property.
	(Effective_Writes_Enabled): Update the call to Has_Enabled_Property.
	(Has_Enabled_Property): Rename formal parameter Extern to State_Id.
	Update comment on usage. Reimplement the logic to recognize the various
	formats of properties.

2014-01-27  Ed Schonberg  <schonberg@adacore.com>

	* par-ch5.adb: Minor reformatting.

2014-01-27  Tristan Gingold  <gingold@adacore.com>

	* s-tposen.ads: Harmonize style and comments.

2014-01-27  Vincent Celier  <celier@adacore.com>

	* projects.texi: Document that shared library projects, by
	default, cannot import projects that are not shared library
	projects.

2014-01-27  Robert Dewar  <dewar@adacore.com>

	* sem_ch8.adb (Find_Selected_Component): Use Replace instead
	of Rewrite.

2014-01-27  Ed Schonberg  <schonberg@adacore.com>

	* a-suenco.adb, a-suenst.adb (Decode): Raise encoding error if
	any other exception is raised.
	(Convert): If both Input_Scheme and Output_Scheme are UTF_8 it is
	still necessary to perform a conversion in order to remove overlong
	encodings.



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

10 files changed, 422 insertions, 193 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index fc60f65b09d..4ef6ddae443 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,53 @@
+2014-01-27  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* einfo.adb (Has_Option): Reimplemented.
+	* sem_prag.adb (Analyze_Refinement_Clause): Add global
+	variables AR_Constit, AW_Constit, ER_Constit, EW_Constit,
+	External_Constit_Seen and State. Add local variables Body_Ref,
+	Body_Ref_Elmt and Extra_State. Reimplement part of the logic to
+	avoid a cumbersome while pool. Verify the legality of an external
+	state and relevant properties.
+	(Check_External_Property): New routine.
+	(Check_Matching_State): Remove parameter profile
+	and update comment on usage.
+	(Collect_Constituent): Store the
+	relevant external property of a constituent.
+	* sem_util.adb (Async_Readers_Enabled): Update the call to
+	Has_Enabled_Property.
+	(Async_Writers_Enabled): Update the call to Has_Enabled_Property.
+	(Effective_Reads_Enabled): Update the call to Has_Enabled_Property.
+	(Effective_Writes_Enabled): Update the call to Has_Enabled_Property.
+	(Has_Enabled_Property): Rename formal parameter Extern to State_Id.
+	Update comment on usage. Reimplement the logic to recognize the various
+	formats of properties.
+
+2014-01-27  Ed Schonberg  <schonberg@adacore.com>
+
+	* par-ch5.adb: Minor reformatting.
+
+2014-01-27  Tristan Gingold  <gingold@adacore.com>
+
+	* s-tposen.ads: Harmonize style and comments.
+
+2014-01-27  Vincent Celier  <celier@adacore.com>
+
+	* projects.texi: Document that shared library projects, by
+	default, cannot import projects that are not shared library
+	projects.
+
+2014-01-27  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch8.adb (Find_Selected_Component): Use Replace instead
+	of Rewrite.
+
+2014-01-27  Ed Schonberg  <schonberg@adacore.com>
+
+	* a-suenco.adb, a-suenst.adb (Decode): Raise encoding error if
+	any other exception is raised.
+	(Convert): If both Input_Scheme and Output_Scheme are UTF_8 it is
+	still necessary to perform a conversion in order to remove overlong
+	encodings.
+
 2014-01-27  Robert Dewar  <dewar@adacore.com>
 
 	* exp_smem.adb: Minor reformatting.
diff --git a/gcc/ada/a-suenco.adb b/gcc/ada/a-suenco.adb
index d824bb444af..ea83123878b 100644
--- a/gcc/ada/a-suenco.adb
+++ b/gcc/ada/a-suenco.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2010-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -41,9 +41,12 @@ package body Ada.Strings.UTF_Encoding.Conversions is
       Output_BOM    : Boolean := False) return UTF_String
    is
    begin
-      --  Nothing to do if identical schemes
+      --  Nothing to do if identical schemes, but for UTF_8 we need to
+      --  exclude overlong encodings, so need to do the full conversion.
 
-      if Input_Scheme = Output_Scheme then
+      if Input_Scheme = Output_Scheme
+        and then Input_Scheme /= UTF_8
+      then
          return Item;
 
       --  For remaining cases, one or other of the operands is UTF-16BE/LE
diff --git a/gcc/ada/a-suenst.adb b/gcc/ada/a-suenst.adb
index a51c3a066e8..87e5893f16b 100644
--- a/gcc/ada/a-suenst.adb
+++ b/gcc/ada/a-suenst.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---             Copyright (C) 2010-2012, Free Software Foundation, Inc.      --
+--          Copyright (C) 2010-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -158,6 +158,12 @@ package body Ada.Strings.UTF_Encoding.Strings is
       end loop;
 
       return Result (1 .. Len);
+
+   exception
+      --  'Val may have been out of range
+
+      when others =>
+         Raise_Encoding_Error (Iptr - 1);
    end Decode;
 
    --  Decode UTF-16 input to String
diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb
index 578e26b842b..8d81ce8ff26 100644
--- a/gcc/ada/einfo.adb
+++ b/gcc/ada/einfo.adb
@@ -589,10 +589,10 @@ package body Einfo is
    -----------------------
 
    function Has_Option
-     (State   : Entity_Id;
-      Opt_Nam : Name_Id) return Boolean;
-   --  Determine whether abstract state State has a particular option denoted
-   --  by the name Opt_Nam.
+     (State_Id   : Entity_Id;
+      Option_Nam : Name_Id) return Boolean;
+   --  Determine whether abstract state State_Id has particular option denoted
+   --  by the name Option_Nam.
 
    ---------------
    -- Float_Rep --
@@ -609,32 +609,55 @@ package body Einfo is
    ----------------
 
    function Has_Option
-     (State   : Entity_Id;
-      Opt_Nam : Name_Id) return Boolean
+     (State_Id   : Entity_Id;
+      Option_Nam : Name_Id) return Boolean
    is
-      Par : constant Node_Id := Parent (State);
-      Opt : Node_Id;
+      Decl    : constant Node_Id := Parent (State_Id);
+      Opt     : Node_Id;
+      Opt_Nam : Node_Id;
 
    begin
-      pragma Assert (Ekind (State) = E_Abstract_State);
+      pragma Assert (Ekind (State_Id) = E_Abstract_State);
 
-      --  States with options appear as extension aggregates in the tree
+      --  The declaration of abstract states with options appear as an
+      --  extension aggregate. If this is not the case, the option is not
+      --  available.
 
-      if Nkind (Par) = N_Extension_Aggregate then
-         if Opt_Nam = Name_Part_Of then
-            return Present (Component_Associations (Par));
+      if Nkind (Decl) /= N_Extension_Aggregate then
+         return False;
+      end if;
 
-         else
-            Opt := First (Expressions (Par));
-            while Present (Opt) loop
-               if Chars (Opt) = Opt_Nam then
-                  return True;
-               end if;
+      --  Simple options
 
-               Next (Opt);
-            end loop;
+      Opt := First (Expressions (Decl));
+      while Present (Opt) loop
+
+         --  Currently the only simple option allowed is External
+
+         if Nkind (Opt) = N_Identifier
+           and then Chars (Opt) = Name_External
+           and then Chars (Opt) = Option_Nam
+         then
+            return True;
          end if;
-      end if;
+
+         Next (Opt);
+      end loop;
+
+      --  Complex options with various specifiers
+
+      Opt := First (Component_Associations (Decl));
+      while Present (Opt) loop
+         Opt_Nam := First (Choices (Opt));
+
+         if Nkind (Opt_Nam) = N_Identifier
+           and then Chars (Opt_Nam) = Option_Nam
+         then
+            return True;
+         end if;
+
+         Next (Opt);
+      end loop;
 
       return False;
    end Has_Option;
diff --git a/gcc/ada/par-ch5.adb b/gcc/ada/par-ch5.adb
index bf28e23bb9d..779acc34ae9 100644
--- a/gcc/ada/par-ch5.adb
+++ b/gcc/ada/par-ch5.adb
@@ -1739,14 +1739,13 @@ package body Ch5 is
       elsif Prev_Token = Tok_In
         and then Present (Subtype_Indication (Node1))
       then
-
          --  Simplest recovery is to transform it into an element iterator.
          --  Error message on 'in" has already been emitted when parsing the
          --  optional constraint.
 
          Set_Of_Present (Node1);
          Error_Msg_N
-           ("subtype indication is only legal on on element iterator",
+           ("subtype indication is only legal on an element iterator",
               Subtype_Indication (Node1));
 
       else
diff --git a/gcc/ada/projects.texi b/gcc/ada/projects.texi
index e9011e18bbc..af3387492cc 100644
--- a/gcc/ada/projects.texi
+++ b/gcc/ada/projects.texi
@@ -1616,6 +1616,10 @@ implementation part of the library implies minimal post-compilation actions on
 the complete system and potentially no action at all for the rest of the
 system in the case of dynamic SALs.
 
+There is a restriction on shared library projects: by default, they are only
+allowed to import other shared library projects. They are not allowed to
+import non library projects or static library projects.
+
 The GNAT Project Manager takes complete care of the library build, rebuild and
 installation tasks, including recompilation of the source files for which
 objects do not exist or are not up to date, assembly of the library archive, and
diff --git a/gcc/ada/s-tposen.ads b/gcc/ada/s-tposen.ads
index 4bba48b81e3..c5b832ce214 100644
--- a/gcc/ada/s-tposen.ads
+++ b/gcc/ada/s-tposen.ads
@@ -1,14 +1,14 @@
 ------------------------------------------------------------------------------
 --                                                                          --
---                GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS                  --
+--                 GNAT RUN-TIME LIBRARY (GNARL) COMPONENTS                 --
 --                                                                          --
---             SYSTEM.TASKING.PROTECTED_OBJECTS.SINGLE_ENTRY                --
+--               SYSTEM.TASKING.PROTECTED_OBJECTS.SINGLE_ENTRY              --
 --                                                                          --
 --                                  S p e c                                 --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
--- GNARL is free software; you can  redistribute it  and/or modify it under --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
@@ -31,7 +31,7 @@
 
 --  This package provides an optimized version of Protected_Objects.Operations
 --  and Protected_Objects.Entries making the following assumptions:
---
+
 --    PO have only one entry
 --    There is only one caller at a time (No_Entry_Queue)
 --    There is no dynamic priority support (No_Dynamic_Priorities)
@@ -39,17 +39,17 @@
 --      (No_Abort_Statements, Max_Asynchronous_Select_Nesting => 0)
 --    PO are at library level
 --    None of the tasks will terminate (no need for finalization)
---
---  This interface is intended to be used in the ravenscar profile, the
+
+--  This interface is intended to be used in the Ravenscar profile, the
 --  compiler is responsible for ensuring that the conditions mentioned above
 --  are respected, except for the No_Entry_Queue restriction that is checked
 --  dynamically in this package, since the check cannot be performed at compile
 --  time, and is relatively cheap (see body).
---
+
 --  This package is part of the high level tasking interface used by the
 --  compiler to expand Ada 95 tasking constructs into simpler run time calls
 --  (aka GNARLI, GNU Ada Run-time Library Interface)
---
+
 --  Note: the compiler generates direct calls to this interface, via Rtsfind.
 --  Any changes to this interface may require corresponding compiler changes
 --  in exp_ch9.adb and possibly exp_ch7.adb
@@ -191,34 +191,34 @@ package System.Tasking.Protected_Objects.Single_Entry is
    --  to keep track of the runtime state of a protected object.
 
    procedure Lock_Entry (Object : Protection_Entry_Access);
-   --  Lock a protected object for write access. Upon return, the caller
-   --  owns the lock to this object, and no other call to Lock or
-   --  Lock_Read_Only with the same argument will return until the
-   --  corresponding call to Unlock has been made by the caller.
+   --  Lock a protected object for write access. Upon return, the caller owns
+   --  the lock to this object, and no other call to Lock or Lock_Read_Only
+   --  with the same argument will return until the corresponding call to
+   --  Unlock has been made by the caller.
 
    procedure Lock_Read_Only_Entry
      (Object : Protection_Entry_Access);
-   --  Lock a protected object for read access.  Upon return, the caller
-   --  owns the lock for read access, and no other calls to Lock
-   --  with the same argument will return until the corresponding call
-   --  to Unlock has been made by the caller.  Other calls to Lock_Read_Only
-   --  may (but need not) return before the call to Unlock, and the
-   --  corresponding callers will also own the lock for read access.
+   --  Lock a protected object for read access. Upon return, the caller owns
+   --  the lock for read access, and no other calls to Lock with the same
+   --  argument will return until the corresponding call to Unlock has been
+   --  made by the caller. Other calls to Lock_Read_Only may (but need not)
+   --  return before the call to Unlock, and the corresponding callers will
+   --  also own the lock for read access.
 
    procedure Unlock_Entry (Object : Protection_Entry_Access);
-   --  Relinquish ownership of the lock for the object represented by
-   --  the Object parameter.  If this ownership was for write access, or
-   --  if it was for read access where there are no other read access
-   --  locks outstanding, one (or more, in the case of Lock_Read_Only)
-   --  of the tasks waiting on this lock (if any) will be given the
-   --  lock and allowed to return from the Lock or Lock_Read_Only call.
+   --  Relinquish ownership of the lock for the object represented by the
+   --  Object parameter. If this ownership was for write access, or if it was
+   --  for read access where there are no other read access locks outstanding,
+   --  one (or more, in the case of Lock_Read_Only) of the tasks waiting on
+   --  this lock (if any) will be given the lock and allowed to return from
+   --  the Lock or Lock_Read_Only call.
 
    procedure Service_Entry (Object : Protection_Entry_Access);
    --  Service the entry queue of the specified object, executing the
    --  corresponding body of any queued entry call that is waiting on True
    --  barrier. This is used when the state of a protected object may have
-   --  changed, in particular after the execution of the statement sequence of
-   --  a protected procedure.
+   --  changed, in particular after the execution of the statement sequence
+   --  of a protected procedure.
    --
    --  This must be called with abort deferred and with the corresponding
    --  object locked. Object is unlocked on return.
@@ -227,9 +227,10 @@ package System.Tasking.Protected_Objects.Single_Entry is
      (Object              : Protection_Entry_Access;
       Uninterpreted_Data  : System.Address;
       Mode                : Call_Modes);
-   --  Make a protected entry call to the specified object.
-   --  Pend a protected entry call on the protected object represented
-   --  by Object. A pended call is not queued; it may be executed immediately
+   --  Make a protected entry call to the specified object
+   --
+   --  Pend a protected entry call on the protected object represented by
+   --  Object. A pended call is not queued; it may be executed immediately
    --  or queued, depending on the state of the entry barrier.
    --
    --    Uninterpreted_Data
@@ -258,19 +259,18 @@ package System.Tasking.Protected_Objects.Single_Entry is
    procedure Exceptional_Complete_Single_Entry_Body
      (Object : Protection_Entry_Access;
       Ex     : Ada.Exceptions.Exception_Id);
-   --  Perform all of the functions of Complete_Entry_Body. In addition,
-   --  report in Ex the exception whose propagation terminated the entry
-   --  body to the runtime system.
+   --  Perform all of the functions of Complete_Entry_Body. In addition, report
+   --  in Ex the exception whose propagation terminated the entry body to the
+   --  runtime system.
 
-   function Protected_Count_Entry (Object : Protection_Entry)
-     return Natural;
+   function Protected_Count_Entry (Object : Protection_Entry) return Natural;
    --  Return the number of entry calls on Object (0 or 1)
 
-   function Protected_Single_Entry_Caller (Object : Protection_Entry)
-     return Task_Id;
-   --  Return value of E'Caller, where E is the protected entry currently
-   --  being handled. This will only work if called from within an
-   --  entry body, as required by the LRM (C.7.1(14)).
+   function Protected_Single_Entry_Caller
+     (Object : Protection_Entry) return Task_Id;
+   --  Return value of E'Caller, where E is the protected entry currently being
+   --  handled. This will only work if called from within an entry body, as
+   --  required by the LRM (C.7.1(14)).
 
 private
    type Protection_Entry is record
diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb
index c6e23b586d5..aea2a4d2d05 100644
--- a/gcc/ada/sem_ch8.adb
+++ b/gcc/ada/sem_ch8.adb
@@ -6296,8 +6296,9 @@ package body Sem_Ch8 is
                --  If no interpretation as an expanded name is possible, it
                --  must be a selected component of a record returned by a
                --  function call. Reformat prefix as a function call, the rest
-               --  is done by type resolution. If the prefix is procedure or
-               --  entry, as is P.X; this is an error.
+               --  is done by type resolution.
+
+               --  Error if the prefix is procedure or entry, as is P.X
 
                if Ekind (P_Name) /= E_Function
                  and then
@@ -6309,7 +6310,6 @@ package body Sem_Ch8 is
                   --  chain, the candidate package may be anywhere on it.
 
                   if Present (Homonym (Current_Entity (P_Name))) then
-
                      P_Name := Current_Entity (P_Name);
 
                      while Present (P_Name) loop
@@ -6327,6 +6327,7 @@ package body Sem_Ch8 is
                         Set_Entity (Prefix (N), P_Name);
                         Find_Expanded_Name (N);
                         return;
+
                      else
                         P_Name := Entity (Prefix (N));
                      end if;
@@ -6338,11 +6339,27 @@ package body Sem_Ch8 is
                   Set_Entity (N, Any_Id);
                   Set_Etype (N, Any_Type);
 
+               --  Here we have a function call, so do the reformatting
+
                else
                   Nam := New_Copy (P);
                   Save_Interps (P, Nam);
-                  Rewrite (P,
+
+                  --  We use Replace here because this is one of those cases
+                  --  where the parser has missclassified the node, and we
+                  --  fix things up and then do the semantic analysis on the
+                  --  fixed up node. Normally we do this using one of the
+                  --  Sinfo.CN routines, but this is too tricky for that.
+
+                  --  Note that using Rewrite would be wrong, because we
+                  --  would have a tree where the original node is unanalyzed,
+                  --  and this violates the required interface for ASIS.
+
+                  Replace (P,
                     Make_Function_Call (Sloc (P), Name => Nam));
+
+                  --  Now analyze the reformatted node
+
                   Analyze_Call (P);
                   Analyze_Selected_Component (N);
                end if;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 1d0c96fe4d5..3ddaed2773c 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -22214,24 +22214,44 @@ package body Sem_Prag is
       -------------------------------
 
       procedure Analyze_Refinement_Clause (Clause : Node_Id) is
-         State_Id : Entity_Id := Empty;
-         --  The entity of the state being refined in the current clause
+         AR_Constit : Entity_Id := Empty;
+         AW_Constit : Entity_Id := Empty;
+         ER_Constit : Entity_Id := Empty;
+         EW_Constit : Entity_Id := Empty;
+         --  The entities of external constituents that contain one of the
+         --  following enabled properties: Async_Readers, Async_Writers,
+         --  Effective_Reads and Effective_Writes.
+
+         External_Constit_Seen : Boolean := False;
+         --  Flag used to mark when at least one external constituent is part
+         --  of the state refinement.
 
          Non_Null_Seen : Boolean := False;
          Null_Seen     : Boolean := False;
          --  Flags used to detect multiple uses of null in a single clause or a
          --  mixture of null and non-null constituents.
 
+         State    : Node_Id;
+         State_Id : Entity_Id;
+         --  The state being refined in the current clause
+
          procedure Analyze_Constituent (Constit : Node_Id);
          --  Perform full analysis of a single constituent
 
-         procedure Check_Matching_State
-           (State    : Node_Id;
-            State_Id : Entity_Id);
-         --  Determine whether state State denoted by its name State_Id appears
-         --  in Abstr_States. Emit an error when attempting to re-refine the
-         --  state or when the state is not defined in the package declaration.
-         --  Otherwise remove the state from Abstr_States.
+         procedure Check_External_Property
+           (Prop_Nam : Name_Id;
+            Enabled  : Boolean;
+            Constit  : Entity_Id);
+         --  Determine whether a property denoted by name Prop_Nam is present
+         --  in both the refined state and constituent Constit. Flag Enabled
+         --  should be set when the property applies to the refined state. If
+         --  this is not the case, emit an error message.
+
+         procedure Check_Matching_State;
+         --  Determine whether the state being refined appears in Abstr_States.
+         --  Emit an error when attempting to re-refine the state or when the
+         --  state is not defined in the package declaration. Otherwise remove
+         --  the state from Abstr_States.
 
          -------------------------
          -- Analyze_Constituent --
@@ -22276,6 +22296,29 @@ package body Sem_Prag is
                   --  body declarations end (see routine Analyze_Declarations).
 
                   Set_Has_Visible_Refinement (State_Id);
+
+                  --  When the constituent is external, save its relevant
+                  --  property for further checks.
+
+                  if Async_Readers_Enabled (Constit_Id) then
+                     AR_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
+
+                  if Async_Writers_Enabled (Constit_Id) then
+                     AW_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
+
+                  if Effective_Reads_Enabled (Constit_Id) then
+                     ER_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
+
+                  if Effective_Writes_Enabled (Constit_Id) then
+                     EW_Constit := Constit_Id;
+                     External_Constit_Seen := True;
+                  end if;
                end Collect_Constituent;
 
                --  Local variables
@@ -22426,14 +22469,44 @@ package body Sem_Prag is
             end if;
          end Analyze_Constituent;
 
+         -----------------------------
+         -- Check_External_Property --
+         -----------------------------
+
+         procedure Check_External_Property
+           (Prop_Nam : Name_Id;
+            Enabled  : Boolean;
+            Constit  : Entity_Id)
+         is
+         begin
+            Error_Msg_Name_1 := Prop_Nam;
+
+            --  The property is enabled in the related Abstract_State pragma
+            --  that defines the state.
+
+            if Enabled then
+               if No (Constit) then
+                  Error_Msg_NE
+                    ("external state & requires at least one constituent with "
+                     & "property % (SPARK RM 7.2.8(3))", State, State_Id);
+               end if;
+
+            --  The property is missing in the declaration of the state, but a
+            --  constituent is introducing it in the state refinement.
+
+            elsif Present (Constit) then
+               Error_Msg_Name_2 := Chars (Constit);
+               Error_Msg_NE
+                 ("external state & lacks property % set by constituent % "
+                  & "(SPARK RM 7.2.8(3))", State, State_Id);
+            end if;
+         end Check_External_Property;
+
          --------------------------
          -- Check_Matching_State --
          --------------------------
 
-         procedure Check_Matching_State
-           (State    : Node_Id;
-            State_Id : Entity_Id)
-         is
+         procedure Check_Matching_State is
             State_Elmt : Elmt_Id;
 
          begin
@@ -22478,8 +22551,10 @@ package body Sem_Prag is
 
          --  Local declarations
 
-         Constit : Node_Id;
-         State   : Node_Id;
+         Body_Ref      : Node_Id;
+         Body_Ref_Elmt : Elmt_Id;
+         Constit       : Node_Id;
+         Extra_State   : Node_Id;
 
       --  Start of processing for Analyze_Refinement_Clause
 
@@ -22487,67 +22562,60 @@ package body Sem_Prag is
          --  Analyze the state name of a refinement clause
 
          State := First (Choices (Clause));
-         while Present (State) loop
-            if Present (State_Id) then
-               Error_Msg_N
-                 ("refinement clause cannot cover multiple states", State);
 
-            else
-               Analyze       (State);
-               Resolve_State (State);
+         Analyze       (State);
+         Resolve_State (State);
 
-               --  Ensure that the state name denotes a valid abstract state
-               --  that is defined in the spec of the related package.
+         --  Ensure that the state name denotes a valid abstract state that is
+         --  defined in the spec of the related package.
 
-               if Is_Entity_Name (State) then
-                  State_Id := Entity_Of (State);
+         if Is_Entity_Name (State) then
+            State_Id := Entity_Of (State);
 
-                  --  Catch any attempts to re-refine a state or refine a
-                  --  state that is not defined in the package declaration.
+            --  Catch any attempts to re-refine a state or refine a state that
+            --  is not defined in the package declaration.
 
-                  if Ekind (State_Id) = E_Abstract_State then
-                     Check_Matching_State (State, State_Id);
-                  else
-                     Error_Msg_NE
-                       ("& must denote an abstract state", State, State_Id);
-                  end if;
+            if Ekind (State_Id) = E_Abstract_State then
+               Check_Matching_State;
+            else
+               Error_Msg_NE
+                 ("& must denote an abstract state", State, State_Id);
+            end if;
 
-                  --  A global item cannot denote a state abstraction whose
-                  --  refinement is visible, in other words a state abstraction
-                  --  cannot be named within its enclosing package's body other
-                  --  than in its refinement.
+            --  A global item cannot denote a state abstraction whose
+            --  refinement is visible, in other words 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      : Node_Id;
-                        Ref_Elmt : Elmt_Id;
+            if Has_Body_References (State_Id) then
+               Body_Ref_Elmt := First_Elmt (Body_References (State_Id));
+               while Present (Body_Ref_Elmt) loop
+                  Body_Ref := Node (Body_Ref_Elmt);
 
-                     begin
-                        Ref_Elmt := First_Elmt (Body_References (State_Id));
-                        while Present (Ref_Elmt) loop
-                           Ref := Node (Ref_Elmt);
+                  Error_Msg_N
+                    ("global reference to & not allowed (SPARK RM 6.1.4(8))",
+                     Body_Ref);
+                  Error_Msg_Sloc := Sloc (State);
+                  Error_Msg_N ("\refinement of & is visible#", Body_Ref);
 
-                           Error_Msg_N
-                             ("global reference to & not allowed (SPARK RM "
-                              & "6.1.4(8))", Ref);
-                           Error_Msg_Sloc := Sloc (State);
-                           Error_Msg_N ("\refinement of & is visible#", Ref);
+                  Next_Elmt (Body_Ref_Elmt);
+               end loop;
+            end if;
 
-                           Next_Elmt (Ref_Elmt);
-                        end loop;
-                     end;
-                  end if;
+            --  The state name is illegal
 
-               --  The state name is illegal
+         else
+            Error_Msg_N ("malformed state name in refinement clause", State);
+         end if;
 
-               else
-                  Error_Msg_N
-                    ("malformed state name in refinement clause", State);
-               end if;
-            end if;
+         --  A refinement clause may only refine one state at a time
 
-            Next (State);
-         end loop;
+         Extra_State := Next (State);
+
+         if Present (Extra_State) then
+            Error_Msg_N
+              ("refinement clause cannot cover multiple states", Extra_State);
+         end if;
 
          --  Analyze all constituents of the refinement. Multiple constituents
          --  appear as an aggregate.
@@ -22575,6 +22643,60 @@ package body Sem_Prag is
          else
             Analyze_Constituent (Constit);
          end if;
+
+         --  A refined external state is subject to special rules with respect
+         --  to its properties and constituents.
+
+         if Is_External_State (State_Id) then
+
+            --  The set of properties that all external constituents yield must
+            --  match that of the refined state. There are two cases to detect:
+            --  the refined state lacks a property or has an extra property.
+
+            if External_Constit_Seen then
+               Check_External_Property
+                 (Prop_Nam => Name_Async_Readers,
+                  Enabled  => Async_Readers_Enabled (State_Id),
+                  Constit  => AR_Constit);
+
+               Check_External_Property
+                 (Prop_Nam => Name_Async_Writers,
+                  Enabled  => Async_Writers_Enabled (State_Id),
+                  Constit  => AW_Constit);
+
+               Check_External_Property
+                 (Prop_Nam => Name_Effective_Reads,
+                  Enabled  => Effective_Reads_Enabled (State_Id),
+                  Constit  => ER_Constit);
+
+               Check_External_Property
+                 (Prop_Nam => Name_Effective_Writes,
+                  Enabled  => Effective_Writes_Enabled (State_Id),
+                  Constit  => EW_Constit);
+
+            --  An external state may be refined to null (SPARK RM 7.2.8(2))
+
+            elsif Null_Seen then
+               null;
+
+            --  The external state has constituents, but none of them are
+            --  external.
+
+            else
+               Error_Msg_NE
+                 ("external state & requires at least one external "
+                  & "constituent or null refinement (SPARK RM 7.2.8(2))",
+                  State, State_Id);
+            end if;
+
+         --  When a refined state is not external, it should not have external
+         --  constituents.
+
+         elsif External_Constit_Seen then
+            Error_Msg_NE
+              ("non-external state & cannot contain external constituents in "
+               & "refinement (SPARK RM 7.2.8(1))", State, State_Id);
+         end if;
       end Analyze_Refinement_Clause;
 
       ---------------------------
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 284872bfc53..8fc28ef4be8 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -114,11 +114,11 @@ package body Sem_Util is
    --  have a default.
 
    function Has_Enabled_Property
-     (Extern   : Node_Id;
+     (State_Id : Node_Id;
       Prop_Nam : Name_Id) return Boolean;
    --  Subsidiary to routines Async_xxx_Enabled and Effective_xxx_Enabled.
-   --  Given pragma External, determine whether it contains a property denoted
-   --  by its name Prop_Nam and if it does, whether its expression is True.
+   --  Determine whether an abstract state denoted by its entity State_Id has
+   --  enabled property Prop_Name.
 
    function Has_Null_Extension (T : Entity_Id) return Boolean;
    --  T is a derived tagged type. Check whether the type extension is null.
@@ -560,10 +560,7 @@ package body Sem_Util is
    function Async_Readers_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Async_Readers);
+         return Has_Enabled_Property (Id, Name_Async_Readers);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Async_Readers));
@@ -577,10 +574,7 @@ package body Sem_Util is
    function Async_Writers_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Async_Writers);
+         return Has_Enabled_Property (Id, Name_Async_Writers);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Async_Writers));
@@ -4818,10 +4812,7 @@ package body Sem_Util is
    function Effective_Reads_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Effective_Reads);
+         return Has_Enabled_Property (Id, Name_Effective_Reads);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Effective_Reads));
@@ -4835,10 +4826,7 @@ package body Sem_Util is
    function Effective_Writes_Enabled (Id : Entity_Id) return Boolean is
    begin
       if Ekind (Id) = E_Abstract_State then
-         return
-           Has_Enabled_Property
-             (Extern   => Get_Pragma (Id, Pragma_External),
-              Prop_Nam => Name_Effective_Writes);
+         return Has_Enabled_Property (Id, Name_Effective_Writes);
 
       else pragma Assert (Ekind (Id) = E_Variable);
          return Present (Get_Pragma (Id, Pragma_Effective_Writes));
@@ -7182,69 +7170,86 @@ package body Sem_Util is
    --------------------------
 
    function Has_Enabled_Property
-     (Extern   : Node_Id;
+     (State_Id : Node_Id;
       Prop_Nam : Name_Id) return Boolean
    is
-      Prop  : Node_Id;
-      Props : Node_Id := Empty;
+      Decl    : constant Node_Id := Parent (State_Id);
+      Opt     : Node_Id;
+      Opt_Nam : Node_Id;
+      Prop    : Node_Id;
+      Props   : Node_Id;
 
    begin
-      --  The related abstract state or variable do not have an Extern pragma,
-      --  the property in question cannot be set.
+      --  The declaration of an external abstract state appears as an extension
+      --  aggregate. If this is not the case, properties can never be set.
 
-      if No (Extern) then
+      if Nkind (Decl) /= N_Extension_Aggregate then
          return False;
-
-      elsif Nkind (Extern) = N_Component_Association then
-         Props := Expression (Extern);
       end if;
 
-      --  External state with properties
+      --  When External appears as a simple option, it automatically enables
+      --  all properties.
 
-      if Present (Props) then
+      Opt := First (Expressions (Decl));
+      while Present (Opt) loop
+         if Nkind (Opt) = N_Identifier
+           and then Chars (Opt) = Name_External
+         then
+            return True;
+         end if;
 
-         --  Multiple properties appear as an aggregate
+         Next (Opt);
+      end loop;
 
-         if Nkind (Props) = N_Aggregate then
+      --  When External specifies particular properties, inspect those and
+      --  find the desired one (if any).
 
-            --  Simple property form
+      Opt := First (Component_Associations (Decl));
+      while Present (Opt) loop
+         Opt_Nam := First (Choices (Opt));
 
-            Prop := First (Expressions (Props));
-            while Present (Prop) loop
-               if Chars (Prop) = Prop_Nam then
-                  return True;
-               end if;
+         if Nkind (Opt_Nam) = N_Identifier
+           and then Chars (Opt_Nam) = Name_External
+         then
+            Props := Expression (Opt);
 
-               Next (Prop);
-            end loop;
+            --  Multiple properties appear as an aggregate
 
-            --  Property with expression form
+            if Nkind (Props) = N_Aggregate then
 
-            Prop := First (Component_Associations (Props));
-            while Present (Prop) loop
-               if Chars (Prop) = Prop_Nam then
-                  return Is_True (Expr_Value (Expression (Prop)));
-               end if;
+               --  Simple property form
 
-               Next (Prop);
-            end loop;
+               Prop := First (Expressions (Props));
+               while Present (Prop) loop
+                  if Chars (Prop) = Prop_Nam then
+                     return True;
+                  end if;
+
+                  Next (Prop);
+               end loop;
 
-            --  Pragma Extern contains properties, but not the one we want
+               --  Property with expression form
 
-            return False;
+               Prop := First (Component_Associations (Props));
+               while Present (Prop) loop
+                  if Chars (Prop) = Prop_Nam then
+                     return Is_True (Expr_Value (Expression (Prop)));
+                  end if;
+
+                  Next (Prop);
+               end loop;
 
-         --  Single property
+            --  Single property
 
-         else
-            return Chars (Prop) = Prop_Nam;
+            else
+               return Chars (Prop) = Prop_Nam;
+            end if;
          end if;
 
-      --  An external state defined without any properties defaults all
-      --  properties to True;
+         Next (Opt);
+      end loop;
 
-      else
-         return True;
-      end if;
+      return False;
    end Has_Enabled_Property;
 
    --------------------