contracts.adb (Analyze_Object_Contract): Update references to SPARK RM.

2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>

	* contracts.adb (Analyze_Object_Contract): Update references to
	SPARK RM.
	* freeze.adb (Freeze_Entity): Update references to SPARK RM.
	* ghost.adb Add with and use clauses for Sem_Disp.
	(Check_Ghost_Derivation): Removed.
	(Check_Ghost_Overriding):
	Reimplemented.	(Check_Ghost_Policy): Update references to SPARK RM.
	(Check_Ghost_Primitive): New routine.
	(Check_Ghost_Refinement): New routine.	(Is_OK_Ghost_Context):
	Update references to SPARK RM.	(Is_OK_Pragma): Update references
	to SPARK RM. Predicates are now a valid context for references
	to Ghost entities.
	* ghost.ads (Check_Ghost_Derivation): Removed.
	(Check_Ghost_Overriding): Update the comment on usage.
	(Check_Ghost_Primitive): New routine.
	(Check_Ghost_Refinement): New routine.
	(Remove_Ignored_Ghost_Code): Update references to SPARK RM.
	* sem_ch3.adb (Process_Full_View): Remove the now obsolete check
	related to Ghost derivations
	* sem_ch6.adb (Check_Conformance): Remove now obsolete check
	related to the convention-like behavior of pragma Ghost.
	(Check_For_Primitive_Subprogram): Verify that the Ghost policy
	of a tagged type and its primitive agree.
	* sem_prag.adb (Analyze_Pragma): Update references to SPARK
	RM. Move the verification of pragma Assertion_Policy Ghost
	to the proper place. Remove the now obsolete check related
	to Ghost derivations.
	(Collect_Constituent): Add a call to Check_Ghost_Refinement.
	* sem_res.adb (Resolve_Actuals): Update references to SPARK RM.

From-SVN: r235115

9 files changed, 326 insertions, 192 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index e59b067..9691433 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,35 @@
+2016-04-18  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* contracts.adb (Analyze_Object_Contract): Update references to
+	SPARK RM.
+	* freeze.adb (Freeze_Entity): Update references to SPARK RM.
+	* ghost.adb Add with and use clauses for Sem_Disp.
+	(Check_Ghost_Derivation): Removed.
+	(Check_Ghost_Overriding):
+	Reimplemented.	(Check_Ghost_Policy): Update references to SPARK RM.
+	(Check_Ghost_Primitive): New routine.
+	(Check_Ghost_Refinement): New routine.	(Is_OK_Ghost_Context):
+	Update references to SPARK RM.	(Is_OK_Pragma): Update references
+	to SPARK RM. Predicates are now a valid context for references
+	to Ghost entities.
+	* ghost.ads (Check_Ghost_Derivation): Removed.
+	(Check_Ghost_Overriding): Update the comment on usage.
+	(Check_Ghost_Primitive): New routine.
+	(Check_Ghost_Refinement): New routine.
+	(Remove_Ignored_Ghost_Code): Update references to SPARK RM.
+	* sem_ch3.adb (Process_Full_View): Remove the now obsolete check
+	related to Ghost derivations
+	* sem_ch6.adb (Check_Conformance): Remove now obsolete check
+	related to the convention-like behavior of pragma Ghost.
+	(Check_For_Primitive_Subprogram): Verify that the Ghost policy
+	of a tagged type and its primitive agree.
+	* sem_prag.adb (Analyze_Pragma): Update references to SPARK
+	RM. Move the verification of pragma Assertion_Policy Ghost
+	to the proper place. Remove the now obsolete check related
+	to Ghost derivations.
+	(Collect_Constituent): Add a call to Check_Ghost_Refinement.
+	* sem_res.adb (Resolve_Actuals): Update references to SPARK RM.
+
 2016-04-18  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* layout.adb: Fix more minor typos in comments.
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 4eb6d26..35a9fd0 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -907,13 +907,13 @@ package body Contracts is
          if Yields_Synchronized_Object (Obj_Typ) then
             Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
 
-         --  A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and
+         --  A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and
          --  SPARK RM 6.9(19)).
 
          elsif Is_Effectively_Volatile (Obj_Id) then
             Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
 
-         --  A Ghost object cannot be imported or exported (SPARK RM 6.9(8)).
+         --  A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
          --  One exception to this is the object that represents the dispatch
          --  table of a Ghost tagged type, as the symbol needs to be exported.
 
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 736535e..556c23a 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -3466,8 +3466,8 @@ package body Freeze is
 
            and then Convention (E) /= Convention_Intrinsic
 
-            --  Assume that ASM interface knows what it is doing. This deals
-            --  with unsigned.ads in the AAMP back end.
+           --  Assume that ASM interface knows what it is doing. This deals
+           --  with unsigned.ads in the AAMP back end.
 
            and then Convention (E) /= Convention_Assembler
          then
@@ -5213,7 +5213,7 @@ package body Freeze is
             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))
+            --  A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
 
             elsif Is_Effectively_Volatile (E) then
                Error_Msg_N ("ghost type & cannot be volatile", E);
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index f2ac16b..9d01b6d 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -36,6 +36,7 @@ with Nmake;    use Nmake;
 with Opt;      use Opt;
 with Sem;      use Sem;
 with Sem_Aux;  use Sem_Aux;
+with Sem_Disp; use Sem_Disp;
 with Sem_Eval; use Sem_Eval;
 with Sem_Prag; use Sem_Prag;
 with Sem_Res;  use Sem_Res;
@@ -154,7 +155,7 @@ package body Ghost is
 
       function Is_OK_Ghost_Context (Context : Node_Id) return Boolean;
       --  Determine whether node Context denotes a Ghost-friendly context where
-      --  a Ghost entity can safely reside.
+      --  a Ghost entity can safely reside (SPARK RM 6.9(10)).
 
       -------------------------
       -- Is_OK_Ghost_Context --
@@ -334,30 +335,19 @@ package body Ghost is
                   return True;
 
                --  An assertion expression pragma is Ghost when it contains a
-               --  reference to a Ghost entity (SPARK RM 6.9(11)).
+               --  reference to a Ghost entity (SPARK RM 6.9(10)).
 
                elsif Assertion_Expression_Pragma (Prag_Id) then
 
-                  --  Predicates are excluded from this category when they do
-                  --  not apply to a Ghost subtype (SPARK RM 6.9(11)).
+                  --  Ensure that the assertion policy and the Ghost policy are
+                  --  compatible (SPARK RM 6.9(18)).
 
-                  if Nam_In (Prag_Nam, Name_Dynamic_Predicate,
-                                       Name_Predicate,
-                                       Name_Static_Predicate)
-                  then
-                     return False;
-
-                  --  Otherwise ensure that the assertion policy and the Ghost
-                  --  policy are compatible (SPARK RM 6.9(18)).
-
-                  else
-                     Check_Policies (Prag_Nam);
-                     return True;
-                  end if;
+                  Check_Policies (Prag_Nam);
+                  return True;
 
                --  Several pragmas that may apply to a non-Ghost entity are
                --  treated as Ghost when they contain a reference to a Ghost
-               --  entity (SPARK RM 6.9(12)).
+               --  entity (SPARK RM 6.9(11)).
 
                elsif Nam_In (Prag_Nam, Name_Global,
                                        Name_Depends,
@@ -455,7 +445,7 @@ package body Ghost is
                   return True;
 
                --  A reference to a Ghost entity can appear within an aspect
-               --  specification (SPARK RM 6.9(11)).
+               --  specification (SPARK RM 6.9(10)).
 
                elsif Nkind (Par) = N_Aspect_Specification then
                   return True;
@@ -504,7 +494,7 @@ package body Ghost is
 
       begin
          --  The Ghost policy in effect a the point of declaration and at the
-         --  point of use must match (SPARK RM 6.9(14)).
+         --  point of use must match (SPARK RM 6.9(13)).
 
          if Is_Checked_Ghost_Entity (Id) and then Policy = Name_Ignore then
             Error_Msg_Sloc := Sloc (Err_N);
@@ -541,48 +531,6 @@ package body Ghost is
    end Check_Ghost_Context;
 
    ----------------------------
-   -- Check_Ghost_Derivation --
-   ----------------------------
-
-   procedure Check_Ghost_Derivation (Typ : Entity_Id) is
-      Parent_Typ : constant Entity_Id := Etype (Typ);
-      Iface      : Entity_Id;
-      Iface_Elmt : Elmt_Id;
-
-   begin
-      --  Allow untagged derivations from predefined types such as Integer as
-      --  those are not Ghost by definition.
-
-      if Is_Scalar_Type (Typ) and then Parent_Typ = Base_Type (Typ) then
-         null;
-
-      --  The parent type of a Ghost type extension must be Ghost
-
-      elsif not Is_Ghost_Entity (Parent_Typ) then
-         Error_Msg_N  ("type extension & cannot be ghost", Typ);
-         Error_Msg_NE ("\parent type & is not ghost", Typ, Parent_Typ);
-         return;
-      end if;
-
-      --  All progenitors (if any) must be Ghost as well
-
-      if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then
-         Iface_Elmt := First_Elmt (Interfaces (Typ));
-         while Present (Iface_Elmt) loop
-            Iface := Node (Iface_Elmt);
-
-            if not Is_Ghost_Entity (Iface) then
-               Error_Msg_N  ("type extension & cannot be ghost", Typ);
-               Error_Msg_NE ("\interface type & is not ghost",   Typ, Iface);
-               return;
-            end if;
-
-            Next_Elmt (Iface_Elmt);
-         end loop;
-      end if;
-   end Check_Ghost_Derivation;
-
-   ----------------------------
    -- Check_Ghost_Overriding --
    ----------------------------
 
@@ -590,40 +538,234 @@ package body Ghost is
      (Subp            : Entity_Id;
       Overridden_Subp : Entity_Id)
    is
+      Deriv_Typ : Entity_Id;
       Over_Subp : Entity_Id;
 
    begin
       if Present (Subp) and then Present (Overridden_Subp) then
          Over_Subp := Ultimate_Alias (Overridden_Subp);
+         Deriv_Typ := Find_Dispatching_Type (Subp);
 
-         --  The Ghost policy in effect at the point of declaration of a parent
-         --  and an overriding subprogram must match (SPARK RM 6.9(17)).
+         --  A Ghost primitive of a non-Ghost type extension cannot override an
+         --  inherited non-Ghost primitive (SPARK RM 6.9(8)).
 
-         if Is_Checked_Ghost_Entity (Over_Subp)
-           and then Is_Ignored_Ghost_Entity (Subp)
+         if Is_Ghost_Entity (Subp)
+           and then Present (Deriv_Typ)
+           and then not Is_Ghost_Entity (Deriv_Typ)
+           and then not Is_Ghost_Entity (Over_Subp)
          then
-            Error_Msg_N ("incompatible ghost policies in effect",    Subp);
+            Error_Msg_N ("incompatible overriding in effect", Subp);
 
             Error_Msg_Sloc := Sloc (Over_Subp);
-            Error_Msg_N ("\& declared # with ghost policy `Check`",  Subp);
+            Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
 
             Error_Msg_Sloc := Sloc (Subp);
-            Error_Msg_N ("\overridden # with ghost policy `Ignore`", Subp);
+            Error_Msg_N ("\overridden # with ghost subprogram", Subp);
+         end if;
+
+         --  A non-Ghost primitive of a type extension cannot override an
+         --  inherited Ghost primitive (SPARK RM 6.9(8)).
 
-         elsif Is_Ignored_Ghost_Entity (Over_Subp)
-           and then Is_Checked_Ghost_Entity (Subp)
+         if not Is_Ghost_Entity (Subp)
+           and then Is_Ghost_Entity (Over_Subp)
          then
-            Error_Msg_N ("incompatible ghost policies in effect",    Subp);
+            Error_Msg_N ("incompatible overriding in effect", Subp);
 
             Error_Msg_Sloc := Sloc (Over_Subp);
-            Error_Msg_N ("\& declared # with ghost policy `Ignore`", Subp);
+            Error_Msg_N ("\& declared # as ghost subprogram", Subp);
 
             Error_Msg_Sloc := Sloc (Subp);
-            Error_Msg_N ("\overridden # with ghost policy `Check`",  Subp);
+            Error_Msg_N ("\overridden # with non-ghost subprogram", Subp);
+         end if;
+
+         if Present (Deriv_Typ)
+           and then not Is_Ignored_Ghost_Entity (Deriv_Typ)
+         then
+            --  When a tagged type is either non-Ghost or checked Ghost and
+            --  one of its primitives overrides an inherited operation, the
+            --  overridden operation of the ancestor type must be ignored Ghost
+            --  if the primitive is ignored Ghost (SPARK RM 6.9(17)).
+
+            if Is_Ignored_Ghost_Entity (Subp) then
+
+               --  Both the parent subprogram and overriding subprogram are
+               --  ignored Ghost.
+
+               if Is_Ignored_Ghost_Entity (Over_Subp) then
+                  null;
+
+               --  The parent subprogram carries policy Check
+
+               elsif Is_Checked_Ghost_Entity (Over_Subp) then
+                  Error_Msg_N
+                    ("incompatible ghost policies in effect", Subp);
+
+                  Error_Msg_Sloc := Sloc (Over_Subp);
+                  Error_Msg_N
+                    ("\& declared # with ghost policy `Check`", Subp);
+
+                  Error_Msg_Sloc := Sloc (Subp);
+                  Error_Msg_N
+                    ("\overridden # with ghost policy `Ignore`", Subp);
+
+               --  The parent subprogram is non-Ghost
+
+               else
+                  Error_Msg_N
+                    ("incompatible ghost policies in effect", Subp);
+
+                  Error_Msg_Sloc := Sloc (Over_Subp);
+                  Error_Msg_N ("\& declared # as non-ghost subprogram", Subp);
+
+                  Error_Msg_Sloc := Sloc (Subp);
+                  Error_Msg_N
+                    ("\overridden # with ghost policy `Ignore`", Subp);
+               end if;
+
+            --  When a tagged type is either non-Ghost or checked Ghost and
+            --  one of its primitives overrides an inherited operation, the
+            --  the primitive of the tagged type must be ignored Ghost if the
+            --  overridden operation is ignored Ghost (SPARK RM 6.9(17)).
+
+            elsif Is_Ignored_Ghost_Entity (Over_Subp) then
+
+               --  Both the parent subprogram and the overriding subprogram are
+               --  ignored Ghost.
+
+               if Is_Ignored_Ghost_Entity (Subp) then
+                  null;
+
+               --  The overriding subprogram carries policy Check
+
+               elsif Is_Checked_Ghost_Entity (Subp) then
+                  Error_Msg_N
+                    ("incompatible ghost policies in effect", Subp);
+
+                  Error_Msg_Sloc := Sloc (Over_Subp);
+                  Error_Msg_N
+                    ("\& declared # with ghost policy `Ignore`", Subp);
+
+                  Error_Msg_Sloc := Sloc (Subp);
+                  Error_Msg_N
+                    ("\overridden # with Ghost policy `Check`", Subp);
+
+               --  The overriding subprogram is non-Ghost
+
+               else
+                  Error_Msg_N
+                    ("incompatible ghost policies in effect", Subp);
+
+                  Error_Msg_Sloc := Sloc (Over_Subp);
+                  Error_Msg_N
+                    ("\& declared # with ghost policy `Ignore`", Subp);
+
+                  Error_Msg_Sloc := Sloc (Subp);
+                  Error_Msg_N
+                    ("\overridden # with non-ghost subprogram", Subp);
+               end if;
+            end if;
          end if;
       end if;
    end Check_Ghost_Overriding;
 
+   ---------------------------
+   -- Check_Ghost_Primitive --
+   ---------------------------
+
+   procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id) is
+   begin
+      --  The Ghost policy in effect at the point of declaration of a primitive
+      --  operation and a tagged type must match (SPARK RM 6.9(16)).
+
+      if Is_Tagged_Type (Typ) then
+         if Is_Checked_Ghost_Entity (Prim)
+           and then Is_Ignored_Ghost_Entity (Typ)
+         then
+            Error_Msg_N ("incompatible ghost policies in effect", Prim);
+
+            Error_Msg_Sloc := Sloc (Typ);
+            Error_Msg_NE
+              ("\tagged type & declared # with ghost policy `Ignore`",
+               Prim, Typ);
+
+            Error_Msg_Sloc := Sloc (Prim);
+            Error_Msg_N
+              ("\primitive subprogram & declared # with ghost policy `Check`",
+               Prim);
+
+         elsif Is_Ignored_Ghost_Entity (Prim)
+           and then Is_Checked_Ghost_Entity (Typ)
+         then
+            Error_Msg_N ("incompatible ghost policies in effect", Prim);
+
+            Error_Msg_Sloc := Sloc (Typ);
+            Error_Msg_NE
+              ("\tagged type & declared # with ghost policy `Check`",
+               Prim, Typ);
+
+            Error_Msg_Sloc := Sloc (Prim);
+            Error_Msg_N
+              ("\primitive subprogram & declared # with ghost policy `Ignore`",
+               Prim);
+         end if;
+      end if;
+   end Check_Ghost_Primitive;
+
+   ----------------------------
+   -- Check_Ghost_Refinement --
+   ----------------------------
+
+   procedure Check_Ghost_Refinement
+     (State      : Node_Id;
+      State_Id   : Entity_Id;
+      Constit    : Node_Id;
+      Constit_Id : Entity_Id)
+   is
+   begin
+      if Is_Ghost_Entity (State_Id) then
+         if Is_Ghost_Entity (Constit_Id) then
+
+            --  The Ghost policy in effect at the point of abstract state
+            --  declaration and constituent must match (SPARK RM 6.9(15)).
+
+            if Is_Checked_Ghost_Entity (State_Id)
+              and then Is_Ignored_Ghost_Entity (Constit_Id)
+            then
+               Error_Msg_Sloc := Sloc (Constit);
+               SPARK_Msg_N ("incompatible ghost policies in effect", State);
+
+               SPARK_Msg_NE
+                 ("\abstract state & declared with ghost policy `Check`",
+                  State, State_Id);
+               SPARK_Msg_NE
+                 ("\constituent & declared # with ghost policy `Ignore`",
+                  State, Constit_Id);
+
+            elsif Is_Ignored_Ghost_Entity (State_Id)
+              and then Is_Checked_Ghost_Entity (Constit_Id)
+            then
+               Error_Msg_Sloc := Sloc (Constit);
+               SPARK_Msg_N ("incompatible ghost policies in effect", State);
+
+               SPARK_Msg_NE
+                 ("\abstract state & declared with ghost policy `Ignore`",
+                  State, State_Id);
+               SPARK_Msg_NE
+                 ("\constituent & declared # with ghost policy `Check`",
+                  State, Constit_Id);
+            end if;
+
+            --  A constituent of a Ghost abstract state must be a Ghost entity
+            --  (SPARK RM 7.2.2(12)).
+
+         else
+            SPARK_Msg_NE
+              ("constituent of ghost state & must be ghost",
+               Constit, State_Id);
+         end if;
+      end if;
+   end Check_Ghost_Refinement;
+
    ------------------
    -- Ghost_Entity --
    ------------------
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index 3dbe502..7a0aec3 100644
--- a/gcc/ada/ghost.ads
+++ b/gcc/ada/ghost.ads
@@ -45,16 +45,25 @@ package Ghost is
    --  Determine whether node Ghost_Ref appears within a Ghost-friendly context
    --  where Ghost entity Ghost_Id can safely reside.
 
-   procedure Check_Ghost_Derivation (Typ : Entity_Id);
-   --  Verify that the parent type and all progenitors of derived type or type
-   --  extension Typ are Ghost. If this is not the case, issue an error.
-
    procedure Check_Ghost_Overriding
      (Subp            : Entity_Id;
       Overridden_Subp : Entity_Id);
-   --  Verify that the Ghost policy of parent subprogram Overridden_Subp is the
-   --  same as the Ghost policy of overriding subprogram Subp. Emit an error if
-   --  this is not the case.
+   --  Verify that the Ghost policy of parent subprogram Overridden_Subp is
+   --  compatible with the Ghost policy of overriding subprogram Subp. Emit
+   --  an error if this is not the case.
+
+   procedure Check_Ghost_Primitive (Prim : Entity_Id; Typ : Entity_Id);
+   --  Verify that the Ghost policy of primitive operation Prim is the same as
+   --  the Ghost policy of tagged type Typ. Emit an error if this is not the
+   --  case.
+
+   procedure Check_Ghost_Refinement
+     (State      : Node_Id;
+      State_Id   : Entity_Id;
+      Constit    : Node_Id;
+      Constit_Id : Entity_Id);
+   --  Verify that the Ghost policy of constituent Constit_Id is compatible
+   --  with the Ghost policy of abstract state State_I.
 
    function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
    --  Determine whether type Typ implements at least one Ghost interface
@@ -85,7 +94,7 @@ package Ghost is
 
    procedure Remove_Ignored_Ghost_Code;
    --  Remove all code marked as ignored Ghost from the trees of all qualifying
-   --  units.
+   --  units (SPARK RM 6.9(4)).
    --
    --  WARNING: this is a separate front end pass, care should be taken to keep
    --  it optimized.
diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb
index a010b54c..d401bd1 100644
--- a/gcc/ada/sem_ch3.adb
+++ b/gcc/ada/sem_ch3.adb
@@ -14649,8 +14649,8 @@ package body Sem_Ch3 is
       then
          Set_Derived_Name;
 
-      --  Otherwise, the type is inheriting a private operation, so enter
-      --  it with a special name so it can't be overridden.
+      --  Otherwise, the type is inheriting a private operation, so enter it
+      --  with a special name so it can't be overridden.
 
       else
          Set_Chars (New_Subp, New_External_Name (Chars (Parent_Subp), 'P'));
@@ -19956,14 +19956,6 @@ package body Sem_Ch3 is
 
          Check_Ghost_Completion (Priv_T, Full_T);
 
-         --  In the case where the private view of a tagged type lacks a parent
-         --  type and is subject to pragma Ghost, ensure that the parent type
-         --  specified by the full view is also Ghost (SPARK RM 6.9(9)).
-
-         if Is_Derived_Type (Full_T) then
-            Check_Ghost_Derivation (Full_T);
-         end if;
-
          --  Propagate the attributes related to pragma Ghost from the private
          --  to the full view.
 
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 437ca14..17c2623 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -4701,18 +4701,6 @@ package body Sem_Ch6 is
          then
             Conformance_Error ("\formal subprograms not allowed!");
             return;
-
-         --  Pragma Ghost behaves as a convention in the context of subtype
-         --  conformance (SPARK RM 6.9(5)). Do not check internally generated
-         --  subprograms as their spec may reside in a Ghost region and their
-         --  body not, or vice versa.
-
-         elsif Comes_From_Source (Old_Id)
-           and then Comes_From_Source (New_Id)
-           and then Is_Ghost_Entity (Old_Id) /= Is_Ghost_Entity (New_Id)
-         then
-            Conformance_Error ("\ghost modes do not match!");
-            return;
          end if;
       end if;
 
@@ -9014,6 +9002,12 @@ package body Sem_Ch6 is
                   Set_Has_Primitive_Operations (B_Typ);
                   Set_Is_Primitive (S);
                   Check_Private_Overriding (B_Typ);
+
+                  --  The Ghost policy in effect at the point of declaration of
+                  --  a tagged type and a primitive operation must match
+                  --  (SPARK RM 6.9(16)).
+
+                  Check_Ghost_Primitive (S, B_Typ);
                end if;
             end if;
 
@@ -9041,6 +9035,12 @@ package body Sem_Ch6 is
                   Set_Is_Primitive (S);
                   Set_Has_Primitive_Operations (B_Typ);
                   Check_Private_Overriding (B_Typ);
+
+                  --  The Ghost policy in effect at the point of declaration of
+                  --  a tagged type and a primitive operation must match
+                  --  (SPARK RM 6.9(16)).
+
+                  Check_Ghost_Primitive (S, B_Typ);
                end if;
 
                Next_Formal (Formal);
@@ -9068,6 +9068,12 @@ package body Sem_Ch6 is
                Set_Is_Primitive (S);
                Set_Has_Primitive_Operations (B_Typ);
                Check_Private_Overriding (B_Typ);
+
+               --  The Ghost policy in effect at the point of declaration of a
+               --  tagged type and a primitive operation must match
+               --  (SPARK RM 6.9(16)).
+
+               Check_Ghost_Primitive (S, B_Typ);
             end if;
          end if;
       end Check_For_Primitive_Subprogram;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 46a3039..e951804 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -11585,7 +11585,8 @@ package body Sem_Prag is
 
                   --  Check Kind and Policy have allowed forms
 
-                  Kind := Chars (Arg);
+                  Kind   := Chars (Arg);
+                  Policy := Get_Pragma_Arg (Arg);
 
                   if not Is_Valid_Assertion_Kind (Kind) then
                      Error_Pragma_Arg
@@ -11595,6 +11596,30 @@ package body Sem_Prag is
                   Check_Arg_Is_One_Of
                     (Arg, Name_Check, Name_Disable, Name_Ignore);
 
+                  if Kind = Name_Ghost then
+
+                     --  The Ghost policy must be either Check or Ignore
+                     --  (SPARK RM 6.9(6)).
+
+                     if not Nam_In (Chars (Policy), Name_Check,
+                                                    Name_Ignore)
+                     then
+                        Error_Pragma_Arg
+                          ("argument of pragma % Ghost must be Check or "
+                           & "Ignore", Policy);
+                     end if;
+
+                     --  Pragma Assertion_Policy specifying a Ghost policy
+                     --  cannot occur within a Ghost subprogram or package
+                     --  (SPARK RM 6.9(14)).
+
+                     if Ghost_Mode > None then
+                        Error_Pragma
+                          ("pragma % cannot appear within ghost subprogram or "
+                           & "package");
+                     end if;
+                  end if;
+
                   --  Rewrite the Assertion_Policy pragma as a series of
                   --  Check_Policy pragmas of the form:
 
@@ -11612,7 +11637,7 @@ package body Sem_Prag is
                          Make_Pragma_Argument_Association (LocP,
                            Expression => Make_Identifier (LocP, Kind)),
                          Make_Pragma_Argument_Association (LocP,
-                           Expression => Get_Pragma_Arg (Arg)))));
+                           Expression => Policy))));
 
                   Arg := Next (Arg);
                end loop;
@@ -12371,8 +12396,7 @@ package body Sem_Prag is
          --  new form syntax.
 
          when Pragma_Check_Policy => Check_Policy : declare
-            Ident : Node_Id;
-            Kind  : Node_Id;
+            Kind : Node_Id;
 
          begin
             GNAT_Pragma;
@@ -12416,29 +12440,6 @@ package body Sem_Prag is
                Check_Arg_Is_One_Of
                  (Arg2,
                   Name_On, Name_Off, Name_Check, Name_Disable, Name_Ignore);
-               Ident := Get_Pragma_Arg (Arg2);
-
-               if Chars (Kind) = Name_Ghost then
-
-                  --  Pragma Check_Policy specifying a Ghost policy cannot
-                  --  occur within a ghost subprogram or package.
-
-                  if Ghost_Mode > None then
-                     Error_Pragma
-                       ("pragma % cannot appear within ghost subprogram or "
-                        & "package");
-
-                  --  The policy identifier of pragma Ghost must be either
-                  --  Check or Ignore (SPARK RM 6.9(7)).
-
-                  elsif not Nam_In (Chars (Ident), Name_Check,
-                                                   Name_Ignore)
-                  then
-                     Error_Pragma_Arg
-                       ("argument of pragma % Ghost must be Check or Ignore",
-                        Arg2);
-                  end if;
-               end if;
 
                --  And chain pragma on the Check_Policy_List for search
 
@@ -15021,14 +15022,6 @@ package body Sem_Prag is
                return;
             end if;
 
-            --  A derived type or type extension cannot be subject to pragma
-            --  Ghost if either the parent type or one of the progenitor types
-            --  is not Ghost (SPARK RM 6.9(9)).
-
-            if Is_Derived_Type (Id) then
-               Check_Ghost_Derivation (Id);
-            end if;
-
             --  Handle completions of types and constants that are subject to
             --  pragma Ghost.
 
@@ -15040,7 +15033,7 @@ package body Sem_Prag is
 
                   --  The full declaration of a deferred constant cannot be
                   --  subject to pragma Ghost unless the deferred declaration
-                  --  is also Ghost (SPARK RM 6.9(10)).
+                  --  is also Ghost (SPARK RM 6.9(9)).
 
                   if Ekind (Prev_Id) = E_Constant then
                      Error_Msg_Name_1 := Pname;
@@ -15058,7 +15051,7 @@ package body Sem_Prag is
 
                   --  The full declaration of a type cannot be subject to
                   --  pragma Ghost unless the partial view is also Ghost
-                  --  (SPARK RM 6.9(10)).
+                  --  (SPARK RM 6.9(9)).
 
                   else
                      Error_Msg_NE (Fix_Error
@@ -15092,7 +15085,7 @@ package body Sem_Prag is
                if Is_OK_Static_Expression (Expr) then
 
                   --  "Ghostness" cannot be turned off once enabled within a
-                  --  region (SPARK RM 6.9(7)).
+                  --  region (SPARK RM 6.9(6)).
 
                   if Is_False (Expr_Value (Expr))
                     and then Ghost_Mode > None
@@ -25230,51 +25223,11 @@ package body Sem_Prag is
 
                procedure Collect_Constituent is
                begin
-                  if Is_Ghost_Entity (State_Id) then
-                     if Is_Ghost_Entity (Constit_Id) then
-
-                        --  The Ghost policy in effect at the point of abstract
-                        --  state declaration and constituent must match
-                        --  (SPARK RM 6.9(16)).
-
-                        if Is_Checked_Ghost_Entity (State_Id)
-                          and then Is_Ignored_Ghost_Entity (Constit_Id)
-                        then
-                           Error_Msg_Sloc := Sloc (Constit);
-
-                           SPARK_Msg_N
-                             ("incompatible ghost policies in effect", State);
-                           SPARK_Msg_NE
-                             ("\abstract state & declared with ghost policy "
-                              & "Check", State, State_Id);
-                           SPARK_Msg_NE
-                             ("\constituent & declared # with ghost policy "
-                              & "Ignore", State, Constit_Id);
-
-                        elsif Is_Ignored_Ghost_Entity (State_Id)
-                          and then Is_Checked_Ghost_Entity (Constit_Id)
-                        then
-                           Error_Msg_Sloc := Sloc (Constit);
-
-                           SPARK_Msg_N
-                             ("incompatible ghost policies in effect", State);
-                           SPARK_Msg_NE
-                             ("\abstract state & declared with ghost policy "
-                              & "Ignore", State, State_Id);
-                           SPARK_Msg_NE
-                             ("\constituent & declared # with ghost policy "
-                              & "Check", State, Constit_Id);
-                        end if;
+                  --  The Ghost policy in effect at the point of abstract state
+                  --  declaration and constituent must match (SPARK RM 6.9(15))
 
-                     --  A constituent of a Ghost abstract state must be a
-                     --  Ghost entity (SPARK RM 7.2.2(12)).
-
-                     else
-                        SPARK_Msg_NE
-                          ("constituent of ghost state & must be ghost",
-                           Constit, State_Id);
-                     end if;
-                  end if;
+                  Check_Ghost_Refinement
+                    (State, State_Id, Constit, Constit_Id);
 
                   --  A synchronized state must be refined by a synchronized
                   --  object or another synchronized state (SPARK RM 9.6).
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index bd4b562..18794c8 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -4528,7 +4528,7 @@ package body Sem_Res is
             end if;
 
             --  The actual parameter of a Ghost subprogram whose formal is of
-            --  mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(13)).
+            --  mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(12)).
 
             if Comes_From_Source (Nam)
               and then Is_Ghost_Entity (Nam)