Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 229374)
+++ sem_prag.adb	(working copy)
@@ -10068,6 +10068,11 @@
                --  Opt is not a duplicate property and sets the flag Status.
                --  (SPARK RM 7.1.4(2))
 
+               procedure Check_Ghost_Synchronous;
+               --  Ensure that the abstract state is not subject to both Ghost
+               --  and Synchronous simple options. Emit an error if this is the
+               --  case.
+
                procedure Create_Abstract_State
                  (Nam     : Name_Id;
                   Decl    : Node_Id;
@@ -10320,6 +10325,20 @@
                   Status := True;
                end Check_Duplicate_Property;
 
+               -----------------------------
+               -- Check_Ghost_Synchronous --
+               -----------------------------
+
+               procedure Check_Ghost_Synchronous is
+               begin
+                  --  A synchronized abstract state cannot be Ghost and vice
+                  --  versa (SPARK RM 6.9(19)).
+
+                  if Ghost_Seen and Synchronous_Seen then
+                     SPARK_Msg_N ("synchronized state cannot be ghost", State);
+                  end if;
+               end Check_Ghost_Synchronous;
+
                ---------------------------
                -- Create_Abstract_State --
                ---------------------------
@@ -10464,6 +10483,7 @@
 
                         elsif Chars (Opt) = Name_Ghost then
                            Check_Duplicate_Option (Opt, Ghost_Seen);
+                           Check_Ghost_Synchronous;
 
                            if Present (State_Id) then
                               Set_Is_Ghost_Entity (State_Id);
@@ -10473,6 +10493,7 @@
 
                         elsif Chars (Opt) = Name_Synchronous then
                            Check_Duplicate_Option (Opt, Synchronous_Seen);
+                           Check_Ghost_Synchronous;
 
                         --  Option Part_Of without an encapsulating state is
                         --  illegal (SPARK RM 7.1.4(9)).
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 229357)
+++ freeze.adb	(working copy)
@@ -2806,6 +2806,15 @@
          then
             Set_Alignment (Arr, Alignment (Component_Type (Arr)));
          end if;
+
+         --  A Ghost type cannot have a component of protected or task type
+         --  (SPARK RM 6.9(19)).
+
+         if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then
+            Error_Msg_N
+              ("ghost array type & cannot have concurrent component type",
+               Arr);
+         end if;
       end Freeze_Array_Type;
 
       -------------------------------
@@ -4341,6 +4350,25 @@
                   Next_Component (Comp);
                end loop;
             end if;
+
+            --  A Ghost type cannot have a component of protected or task type
+            --  (SPARK RM 6.9(19)).
+
+            if Is_Ghost_Entity (Rec) then
+               Comp := First_Component (Rec);
+               while Present (Comp) loop
+                  if Comes_From_Source (Comp)
+                    and then Is_Concurrent_Type (Etype (Comp))
+                  then
+                     Error_Msg_Name_1 := Chars (Rec);
+                     Error_Msg_N
+                       ("component & of ghost type % cannot be concurrent",
+                        Comp);
+                  end if;
+
+                  Next_Component (Comp);
+               end loop;
+            end if;
          end if;
 
          --  Make sure that if we have an iterator aspect, then we have
@@ -5091,12 +5119,19 @@
             end if;
          end;
 
-         --  A Ghost type cannot be effectively volatile (SPARK RM 6.9(8))
+         if Is_Ghost_Entity (E) then
 
-         if Is_Ghost_Entity (E)
-           and then Is_Effectively_Volatile (E)
-         then
-            Error_Msg_N ("ghost type & cannot be volatile", E);
+            --  A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify
+            --  this legality rule first to five a finer-grained diagnostic.
+
+            if Is_Concurrent_Type (E) then
+               Error_Msg_N ("ghost type & cannot be concurrent", E);
+
+            --  A Ghost type cannot be effectively volatile (SPARK RM 6.9(8))
+
+            elsif Is_Effectively_Volatile (E) then
+               Error_Msg_N ("ghost type & cannot be volatile", E);
+            end if;
          end if;
 
          --  Deal with special cases of freezing for subtype
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 229374)
+++ sem_util.adb	(working copy)
@@ -20121,7 +20121,8 @@
    --------------------------------
 
    function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean is
-      Id : Entity_Id;
+      Has_Sync_Comp : Boolean := False;
+      Id            : Entity_Id;
 
    begin
       --  An array type yields a synchronized object if its component type
@@ -20154,11 +20155,16 @@
          Id := First_Entity (Typ);
          while Present (Id) loop
             if Comes_From_Source (Id) then
-               if Ekind (Id) = E_Component
-                 and then not Yields_Synchronized_Object (Etype (Id))
-               then
-                  return False;
+               if Ekind (Id) = E_Component then
+                  if Yields_Synchronized_Object (Etype (Id)) then
+                     Has_Sync_Comp := True;
 
+                  --  The component does not yield a synchronized object
+
+                  else
+                     return False;
+                  end if;
+
                elsif Ekind (Id) = E_Discriminant
                  and then Present (Expression (Parent (Id)))
                then
@@ -20181,7 +20187,7 @@
          --  If we get here, then all discriminants lack default values and all
          --  components are of a type that yields a synchronized object.
 
-         return True;
+         return Has_Sync_Comp;
 
       --  A synchronized interface type yields a synchronized object by default
 
Index: contracts.adb
===================================================================
--- contracts.adb	(revision 229373)
+++ contracts.adb	(working copy)
@@ -648,10 +648,34 @@
          end if;
       end if;
 
+      --  The anonymous object created for a single concurrent type inherits
+      --  the SPARK_Mode from the type. Due to the timing of contract analysis,
+      --  delayed pragmas may be subject to the wrong SPARK_Mode, usually that
+      --  of the enclosing context. To remedy this, restore the original mode
+      --  of the related anonymous object.
+
+      if Is_Single_Concurrent_Object (Obj_Id)
+        and then Present (SPARK_Pragma (Obj_Id))
+      then
+         Restore_Mode := True;
+         Save_SPARK_Mode_And_Set (Obj_Id, Mode);
+      end if;
+
       --  Constant-related checks
 
       if Ekind (Obj_Id) = E_Constant then
 
+         --  Analyze indicator Part_Of
+
+         Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
+
+         --  Check whether the lack of indicator Part_Of agrees with the
+         --  placement of the constant with respect to the state space.
+
+         if No (Prag) then
+            Check_Missing_Part_Of (Obj_Id);
+         end if;
+
          --  A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
          --  This check is relevant only when SPARK_Mode is on, as it is not
          --  a standard Ada legality rule. Internally-generated constants that
@@ -666,32 +690,10 @@
             Error_Msg_N ("constant cannot be volatile", Obj_Id);
          end if;
 
-         Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
-
-         --  Check whether the lack of indicator Part_Of agrees with the
-         --  placement of the constant with respect to the state space.
-
-         if No (Prag) then
-            Check_Missing_Part_Of (Obj_Id);
-         end if;
-
       --  Variable-related checks
 
       else pragma Assert (Ekind (Obj_Id) = E_Variable);
 
-         --  The anonymous object created for a single concurrent type inherits
-         --  the SPARK_Mode from the type. Due to the timing of contract
-         --  analysis, delayed pragmas may be subject to the wrong SPARK_Mode,
-         --  usually that of the enclosing context. To remedy this, restore the
-         --  original SPARK_Mode of the related variable.
-
-         if Is_Single_Concurrent_Object (Obj_Id)
-           and then Present (SPARK_Pragma (Obj_Id))
-         then
-            Restore_Mode := True;
-            Save_SPARK_Mode_And_Set (Obj_Id, Mode);
-         end if;
-
          --  Analyze all external properties
 
          Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
@@ -834,44 +836,42 @@
                   & "protected type %"), Obj_Id);
             end if;
          end if;
+      end if;
 
-         if Is_Ghost_Entity (Obj_Id) then
+      --  Common checks
 
-            --  A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
+      if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
 
-            if Is_Effectively_Volatile (Obj_Id) then
-               Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
+         --  A Ghost object cannot be of a type that yields a synchronized
+         --  object (SPARK RM 6.9(19)).
 
-            --  A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
+         if Yields_Synchronized_Object (Obj_Typ) then
+            Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
 
-            elsif Is_Imported (Obj_Id) then
-               Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
+         --  A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and
+         --  SPARK RM 6.9(19)).
 
-            elsif Is_Exported (Obj_Id) then
-               Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
-            end if;
-         end if;
+         elsif Is_Effectively_Volatile (Obj_Id) then
+            Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
 
-         --  Restore the SPARK_Mode of the enclosing context after all delayed
-         --  pragmas have been analyzed.
+         --  A Ghost object cannot be imported or exported (SPARK RM 6.9(8)).
+         --  One exception to this is the object that represents the dispatch
+         --  table of a Ghost tagged type, as the symbol needs to be exported.
 
-         if Restore_Mode then
-            Restore_SPARK_Mode (Mode);
-         end if;
-      end if;
-
-      --  A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
-      --  exception to this is the object that represents the dispatch table of
-      --  a Ghost tagged type, as the symbol needs to be exported.
-
-      if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
-         if Is_Exported (Obj_Id) then
+         elsif Is_Exported (Obj_Id) then
             Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
 
          elsif Is_Imported (Obj_Id) then
             Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
          end if;
       end if;
+
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
+      if Restore_Mode then
+         Restore_SPARK_Mode (Mode);
+      end if;
    end Analyze_Object_Contract;
 
    -----------------------------------
