[Ada] Derivation of Ghost types

Arnaud Charlet charlet@adacore.com
Mon Apr 18 10:22:00 GMT 2016


This patch implements the following rules from the SPARK RM:

   6.9(8) - A ghost primitive subprogram of a non-ghost type extension shall
   not override an inherited non-ghost primitive subprogram. A non-ghost
   primitive subprogram of a type extension shall not override an inherited
   ghost primitive subprogram.

   6.9(16) - The Ghost assertion policies in effect at the declaration of a
   primitive subprogram of a ghost tagged type and at the declaration of the
   ghost tagged type shall be the same.

   6.9(17) - If a tagged type is not a disabled ghost type, and if a primitive
   operation of the tagged type overrides an inherited operation, then the
   corresponding operation of the ancestor type shall be a disabled ghost
   subprogram if and only if the overriding subprogram is a disabled ghost
   subprogram.

------------
-- Source --
------------

--  bad_ancestor.ads

package Bad_Ancestor with SPARK_Mode is
   type R is tagged null record;

   procedure P   (X : R);                                  --  OK
   pragma Assertion_Policy (Ghost => Check);
   procedure PGC (X : R) with Ghost;                       --  OK
   pragma Assertion_Policy (Ghost => Ignore);
   procedure PGI (X : R) with Ghost;                       --  OK

   pragma Assertion_Policy (Ghost => Check);
   type RGC is tagged null record with Ghost;

   procedure P   (X : RGC);                                --  Error 6.9(10)
   pragma Assertion_Policy (Ghost => Check);
   procedure PGC (X : RGC) with Ghost;                     --  OK
   pragma Assertion_Policy (Ghost => Ignore);
   procedure PGI (X : RGC) with Ghost;                     --  Error 6.9(13,17)

   pragma Assertion_Policy (Ghost => Ignore);
   type RGI is tagged null record with Ghost;

   procedure P   (X : RGI);                                --  Error 6.9(10)
   pragma Assertion_Policy (Ghost => Check);
   procedure PGC (X : RGI) with Ghost;                     --  Error 6.9(13,17)
   pragma Assertion_Policy (Ghost => Ignore);
   procedure PGI (X : RGI) with Ghost;                     --  OK
end Bad_Ancestor;

--  bad_extension.ads

with Bad_Ancestor; use Bad_Ancestor;

package Bad_Extension with SPARK_Mode is
   type E1 is new R with null record;

   overriding procedure P   (X : E1);                      --  OK
   overriding procedure PGC (X : E1);                      --  Error 6.9(8)
   overriding procedure PGI (X : E1);                      --  Error 6.9(8)

   type E2 is new R with null record;

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2) with Ghost;           --  Error 6.9(8)
   overriding procedure PGC (X : E2) with Ghost;           --  OK
   overriding procedure PGI (X : E2) with Ghost;           --  Error 6.9(17)

   type E3 is new R with null record;

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3) with Ghost;           --  Error 6.9(8)
   overriding procedure PGC (X : E3) with Ghost;           --  Error 6.9(17)
   overriding procedure PGI (X : E3) with Ghost;           --  OK

   type E1GC is new RGC with null record;                  --  Error 6.9(10)

   overriding procedure P   (X : E1GC);                    --  Error 6.9(10)
   overriding procedure PGC (X : E1GC);                    --  Error 6.9(8,10)
   overriding procedure PGI (X : E1GC);                    --  Error bad inher

   type E2GC is new RGC with null record;                  --  Error 6.9(10)

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2GC) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGC (X : E2GC) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGI (X : E2GC) with Ghost;         --  Error 6.9(13,16)

   type E3GC is new RGC with null record;                  --  Error 6.9(10)

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3GC) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGC (X : E3GC) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGI (X : E3GC) with Ghost;         --  Error 6.9(13,16)

   type E1GI is new RGI with null record;                  --  Error 6.9(10)

   overriding procedure P   (X : E1GI);                    --  Error 6.9(10)
   overriding procedure PGC (X : E1GI);                    --  Error bad inher
   overriding procedure PGI (X : E1GI);                    --  Error 6.9(8,10)

   type E2GI is new RGI with null record;                  --  Error 6.9(10)

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2GI) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGC (X : E2GI) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGI (X : E2GI) with Ghost;         --  Error 6.9(13,16)

   type E3GI is new RGI with null record;                  --  Error 6.9(10)

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3GI) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGC (X : E3GI) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGI (X : E3GI) with Ghost;         --  Error 6.9(13,16)
end Bad_Extension;

--  bad_extension_ghost_check.ads

with Bad_Ancestor; use Bad_Ancestor;

package Bad_Extension_Ghost_Check with SPARK_Mode is
   pragma Assertion_Policy (Ghost => Check);
   type E1 is new R with null record with Ghost;

   overriding procedure P   (X : E1);                      --  Error 6.9(10)
   overriding procedure PGC (X : E1);                      --  Error 6.9(8,10)
   overriding procedure PGI (X : E1);                      --  Error 6.9(8,10)

   pragma Assertion_Policy (Ghost => Check);
   type E2 is new R with null record with Ghost;

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2) with Ghost;           --  OK
   overriding procedure PGC (X : E2) with Ghost;           --  OK
   overriding procedure PGI (X : E2) with Ghost;           --  Error 6.9(17)

   pragma Assertion_Policy (Ghost => Check);
   type E3 is new R with null record with Ghost;

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3) with Ghost;           --  Error 6.9(13,17)
   overriding procedure PGC (X : E3) with Ghost;           --  Error 6.9(13,17)
   overriding procedure PGI (X : E3) with Ghost;           --  Error 6.9(13,16)

   pragma Assertion_Policy (Ghost => Check);
   type E1GC is new RGC with null record with Ghost;

   overriding procedure P   (X : E1GC);                    --  Error 6.9(10)
   overriding procedure PGC (X : E1GC);                    --  Error 6.9(8,10)
   overriding procedure PGI (X : E1GC);                    --  Error 6.9(10)

   pragma Assertion_Policy (Ghost => Check);
   type E2GC is new RGC with null record with Ghost;

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2GC) with Ghost;         --  ???
   overriding procedure PGC (X : E2GC) with Ghost;         --  OK
   overriding procedure PGI (X : E2GC) with Ghost;         --  Error bad inher

   pragma Assertion_Policy (Ghost => Check);
   type E3GC is new RGC with null record with Ghost;

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3GC) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGC (X : E3GC) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGI (X : E3GC) with Ghost;         --  Error 6.9(13,16)

   pragma Assertion_Policy (Ghost => Check);
   type E1GI is new RGI with null record with Ghost;       --  Error 6.9(13)

   overriding procedure P   (X : E1GI);                    --  Error 6.9(10)
   overriding procedure PGC (X : E1GI);                    --  Error bad inher
   overriding procedure PGI (X : E1GI);                    --  Error 6.9(8)

   pragma Assertion_Policy (Ghost => Check);
   type E2GI is new RGI with null record with Ghost;       --  Error 6.9(13)

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2GI) with Ghost;         --  ???
   overriding procedure PGC (X : E2GI) with Ghost;         --  Error bad inher
   overriding procedure PGI (X : E2GI) with Ghost;         --  Error 6.9(17)

   pragma Assertion_Policy (Ghost => Check);
   type E3GI is new RGI with null record with Ghost;       --  Error 6.9(13)

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3GI) with Ghost;         --  Error 6.9(13,17)
   overriding procedure PGC (X : E3GI) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGI (X : E3GI) with Ghost;         --  Error 6.9(13,16)
end Bad_Extension_Ghost_Check;

--  bad_extension_ghost_ignore.ads

with Bad_Ancestor; use Bad_Ancestor;

package Bad_Extension_Ghost_Ignore with SPARK_Mode is
   pragma Assertion_Policy (Ghost => Ignore);
   type E1 is new R with null record with Ghost;

   overriding procedure P   (X : E1);                      --  Error 6.9(10)
   overriding procedure PGC (X : E1);                      --  Error 6.9(8,10)
   overriding procedure PGI (X : E1);                      --  Error 6.9(8,10)

   pragma Assertion_Policy (Ghost => Ignore);
   type E2 is new R with null record with Ghost;

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2) with Ghost;           --  Error 6.9(13,16)
   overriding procedure PGC (X : E2) with Ghost;           --  Error 6.9(13,16)
   overriding procedure PGI (X : E2) with Ghost;           --  Error 6.9(13,16)

   pragma Assertion_Policy (Ghost => Ignore);
   type E3 is new R with null record with Ghost;

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3) with Ghost;           --  OK
   overriding procedure PGC (X : E3) with Ghost;           --  OK
   overriding procedure PGI (X : E3) with Ghost;           --  OK

   pragma Assertion_Policy (Ghost => Ignore);
   type E1GC is new RGC with null record with Ghost;

   overriding procedure P   (X : E1GC);                    --  Error 6.9(10)
   overriding procedure PGC (X : E1GC);                    --  Error 6.9(8,10)
   overriding procedure PGI (X : E1GC);                    --  Error bad inher

   pragma Assertion_Policy (Ghost => Ignore);
   type E2GC is new RGC with null record with Ghost;       --  Error 6.9(13)

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2GC) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGC (X : E2GC) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGI (X : E2GC) with Ghost;         --  Error 6.9(13,16)

   pragma Assertion_Policy (Ghost => Ignore);
   type E3GC is new RGC with null record with Ghost;       --  Error 6.9(13)

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3GC) with Ghost;         --  ???
   overriding procedure PGC (X : E3GC) with Ghost;         --  OK
   overriding procedure PGI (X : E3GC) with Ghost;         --  Error bad inher

   pragma Assertion_Policy (Ghost => Ignore);
   type E1GI is new RGI with null record with Ghost;

   overriding procedure P   (X : E1GI);                    --  Error 6.9(10)
   overriding procedure PGC (X : E1GI);                    --  Error bad inher
   overriding procedure PGI (X : E1GI);                    --  Error 6.9(8,10)

   pragma Assertion_Policy (Ghost => Ignore);
   type E2GI is new RGI with null record with Ghost;

   pragma Assertion_Policy (Ghost => Check);
   overriding procedure P   (X : E2GI) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGC (X : E2GI) with Ghost;         --  Error 6.9(13,16)
   overriding procedure PGI (X : E2GI) with Ghost;         --  Error 6.9(13,16)

   pragma Assertion_Policy (Ghost => Ignore);
   type E3GI is new RGI with null record with Ghost;

   pragma Assertion_Policy (Ghost => Ignore);
   overriding procedure P   (X : E3GI) with Ghost;         --  ???
   overriding procedure PGC (X : E3GI) with Ghost;         --  Error bad inher
   overriding procedure PGI (X : E3GI) with Ghost;         --  OK
end Bad_Extension_Ghost_Ignore;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c bad_extension.ads
$ gcc -c bad_extension_ghost_check.ads
$ gcc -c bad_extension_ghost_ignore.ads
bad_extension.ads:7:25: incompatible overriding in effect
bad_extension.ads:7:25: "PGC" declared at bad_ancestor.ads:6 as ghost
  subprogram
bad_extension.ads:7:25: overridden at line 7 with non-ghost subprogram
bad_extension.ads:8:25: incompatible overriding in effect
bad_extension.ads:8:25: "PGI" declared at bad_ancestor.ads:8 as ghost
  subprogram
bad_extension.ads:8:25: overridden at line 8 with non-ghost subprogram
bad_extension.ads:13:25: incompatible overriding in effect
bad_extension.ads:13:25: "P" declared at bad_ancestor.ads:4 as non-ghost
  subprogram
bad_extension.ads:13:25: overridden at line 13 with ghost subprogram
bad_extension.ads:15:25: incompatible ghost policies in effect
bad_extension.ads:15:25: "PGI" declared at bad_ancestor.ads:8 with ghost policy
  "Ignore"
bad_extension.ads:15:25: overridden at line 15 with Ghost policy "Check"
bad_extension.ads:20:25: incompatible overriding in effect
bad_extension.ads:20:25: "P" declared at bad_ancestor.ads:4 as non-ghost
  subprogram
bad_extension.ads:20:25: overridden at line 20 with ghost subprogram
bad_extension.ads:21:25: incompatible ghost policies in effect
bad_extension.ads:21:25: "PGC" declared at bad_ancestor.ads:6 with ghost policy
  "Check"
bad_extension.ads:21:25: overridden at line 21 with ghost policy "Ignore"
bad_extension.ads:24:21: ghost entity cannot appear in this context
bad_extension.ads:26:34: ghost entity cannot appear in this context
bad_extension.ads:27:25: incompatible overriding in effect
bad_extension.ads:27:25: "PGC" declared at bad_ancestor.ads:15 as ghost
  subprogram
bad_extension.ads:27:25: overridden at line 27 with non-ghost subprogram
bad_extension.ads:27:34: ghost entity cannot appear in this context
bad_extension.ads:28:15: subprogram "PGI" is not overriding
bad_extension.ads:28:34: ghost entity cannot appear in this context
bad_extension.ads:30:21: ghost entity cannot appear in this context
bad_extension.ads:33:25: incompatible ghost policies in effect
bad_extension.ads:33:25: tagged type "E2GC" declared at line 30 with ghost
  policy "Ignore"
bad_extension.ads:33:25: primitive subprogram "P" declared at line 33 with
  ghost policy "Check"
bad_extension.ads:33:34: incompatible ghost policies in effect
bad_extension.ads:33:34: "E2GC" declared with ghost policy "Ignore"
bad_extension.ads:33:34: "E2GC" used at line 33 with ghost policy "Check"
bad_extension.ads:34:25: incompatible ghost policies in effect
bad_extension.ads:34:25: tagged type "E2GC" declared at line 30 with ghost
  policy "Ignore"
bad_extension.ads:34:25: primitive subprogram "PGC" declared at line 34 with
  ghost policy "Check"
bad_extension.ads:34:34: incompatible ghost policies in effect
bad_extension.ads:34:34: "E2GC" declared with ghost policy "Ignore"
bad_extension.ads:34:34: "E2GC" used at line 34 with ghost policy "Check"
bad_extension.ads:35:25: incompatible ghost policies in effect
bad_extension.ads:35:25: tagged type "E2GC" declared at line 30 with ghost
  policy "Ignore"
bad_extension.ads:35:25: primitive subprogram "PGI" declared at line 35 with
  ghost policy "Check"
bad_extension.ads:35:34: incompatible ghost policies in effect
bad_extension.ads:35:34: "E2GC" declared with ghost policy "Ignore"
bad_extension.ads:35:34: "E2GC" used at line 35 with ghost policy "Check"
bad_extension.ads:37:21: ghost entity cannot appear in this context
bad_extension.ads:40:25: incompatible ghost policies in effect
bad_extension.ads:40:25: "P" declared at bad_ancestor.ads:13 as non-ghost
  subprogram
bad_extension.ads:40:25: overridden at line 40 with ghost policy "Ignore"
bad_extension.ads:40:34: incompatible ghost policies in effect
bad_extension.ads:40:34: "E3GC" declared with ghost policy "Check"
bad_extension.ads:40:34: "E3GC" used at line 40 with ghost policy "Ignore"
bad_extension.ads:41:25: incompatible ghost policies in effect
bad_extension.ads:41:25: "PGC" declared at bad_ancestor.ads:15 with ghost
  policy "Check"
bad_extension.ads:41:25: overridden at line 41 with ghost policy "Ignore"
bad_extension.ads:41:34: incompatible ghost policies in effect
bad_extension.ads:41:34: "E3GC" declared with ghost policy "Check"
bad_extension.ads:41:34: "E3GC" used at line 41 with ghost policy "Ignore"
bad_extension.ads:42:25: incompatible ghost policies in effect
bad_extension.ads:42:25: tagged type "E3GC" declared at line 37 with ghost
  policy "Check"
bad_extension.ads:42:25: primitive subprogram "PGI" declared at line 42 with
  ghost policy "Ignore"
bad_extension.ads:42:34: incompatible ghost policies in effect
bad_extension.ads:42:34: "E3GC" declared with ghost policy "Check"
bad_extension.ads:42:34: "E3GC" used at line 42 with ghost policy "Ignore"
bad_extension.ads:44:21: ghost entity cannot appear in this context
bad_extension.ads:46:34: ghost entity cannot appear in this context
bad_extension.ads:47:15: subprogram "PGC" is not overriding
bad_extension.ads:47:34: ghost entity cannot appear in this context
bad_extension.ads:48:25: incompatible overriding in effect
bad_extension.ads:48:25: "PGI" declared at bad_ancestor.ads:26 as ghost
  subprogram
bad_extension.ads:48:25: overridden at line 48 with non-ghost subprogram
bad_extension.ads:48:34: ghost entity cannot appear in this context
bad_extension.ads:50:21: ghost entity cannot appear in this context
bad_extension.ads:53:25: incompatible ghost policies in effect
bad_extension.ads:53:25: tagged type "E2GI" declared at line 50 with ghost
  policy "Ignore"
bad_extension.ads:53:25: primitive subprogram "P" declared at line 53 with
  ghost policy "Check"
bad_extension.ads:53:34: incompatible ghost policies in effect
bad_extension.ads:53:34: "E2GI" declared with ghost policy "Ignore"
bad_extension.ads:53:34: "E2GI" used at line 53 with ghost policy "Check"
bad_extension.ads:54:25: incompatible ghost policies in effect
bad_extension.ads:54:25: tagged type "E2GI" declared at line 50 with ghost
  policy "Ignore"
bad_extension.ads:54:25: primitive subprogram "PGC" declared at line 54 with
  ghost policy "Check"
bad_extension.ads:54:34: incompatible ghost policies in effect
bad_extension.ads:54:34: "E2GI" declared with ghost policy "Ignore"
bad_extension.ads:54:34: "E2GI" used at line 54 with ghost policy "Check"
bad_extension.ads:55:25: incompatible ghost policies in effect
bad_extension.ads:55:25: tagged type "E2GI" declared at line 50 with ghost
  policy "Ignore"
bad_extension.ads:55:25: primitive subprogram "PGI" declared at line 55 with
  ghost policy "Check"
bad_extension.ads:55:34: incompatible ghost policies in effect
bad_extension.ads:55:34: "E2GI" declared with ghost policy "Ignore"
bad_extension.ads:55:34: "E2GI" used at line 55 with ghost policy "Check"
bad_extension.ads:57:21: ghost entity cannot appear in this context
bad_extension.ads:60:25: incompatible ghost policies in effect
bad_extension.ads:60:25: "P" declared at bad_ancestor.ads:22 as non-ghost
  subprogram
bad_extension.ads:60:25: overridden at line 60 with ghost policy "Ignore"
bad_extension.ads:60:34: incompatible ghost policies in effect
bad_extension.ads:60:34: "E3GI" declared with ghost policy "Check"
bad_extension.ads:60:34: "E3GI" used at line 60 with ghost policy "Ignore"
bad_extension.ads:61:25: incompatible ghost policies in effect
bad_extension.ads:61:25: tagged type "E3GI" declared at line 57 with ghost
  policy "Check"
bad_extension.ads:61:25: primitive subprogram "PGC" declared at line 61 with
  ghost policy "Ignore"
bad_extension.ads:61:34: incompatible ghost policies in effect
bad_extension.ads:61:34: "E3GI" declared with ghost policy "Check"
bad_extension.ads:61:34: "E3GI" used at line 61 with ghost policy "Ignore"
bad_extension.ads:62:25: incompatible ghost policies in effect
bad_extension.ads:62:25: tagged type "E3GI" declared at line 57 with ghost
  policy "Check"
bad_extension.ads:62:25: primitive subprogram "PGI" declared at line 62 with
  ghost policy "Ignore"
bad_extension.ads:62:34: incompatible ghost policies in effect
bad_extension.ads:62:34: "E3GI" declared with ghost policy "Check"
bad_extension.ads:62:34: "E3GI" used at line 62 with ghost policy "Ignore"
bad_ancestor.ads:13:23: ghost entity cannot appear in this context
bad_ancestor.ads:17:14: incompatible ghost policies in effect
bad_ancestor.ads:17:14: tagged type "RGC" declared at line 11 with ghost policy
  "Check"
bad_ancestor.ads:17:14: primitive subprogram "PGI" declared at line 17 with
  ghost policy "Ignore"
bad_ancestor.ads:17:23: incompatible ghost policies in effect
bad_ancestor.ads:17:23: "RGC" declared with ghost policy "Check"
bad_ancestor.ads:17:23: "RGC" used at line 17 with ghost policy "Ignore"
bad_ancestor.ads:22:23: ghost entity cannot appear in this context
bad_ancestor.ads:24:14: incompatible ghost policies in effect
bad_ancestor.ads:24:14: tagged type "RGI" declared at line 20 with ghost policy
  "Ignore"
bad_ancestor.ads:24:14: primitive subprogram "PGC" declared at line 24 with
  ghost policy "Check"
bad_ancestor.ads:24:23: incompatible ghost policies in effect
bad_ancestor.ads:24:23: "RGI" declared with ghost policy "Ignore"
bad_ancestor.ads:24:23: "RGI" used at line 24 with ghost policy "Check"
bad_extension_ghost_check.ads:7:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:8:25: incompatible overriding in effect
bad_extension_ghost_check.ads:8:25: "PGC" declared at bad_ancestor.ads:6 as
  ghost subprogram
bad_extension_ghost_check.ads:8:25: overridden at line 8 with non-ghost
  subprogram
bad_extension_ghost_check.ads:8:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:9:25: incompatible overriding in effect
bad_extension_ghost_check.ads:9:25: "PGI" declared at bad_ancestor.ads:8 as
  ghost subprogram
bad_extension_ghost_check.ads:9:25: overridden at line 9 with non-ghost
  subprogram
bad_extension_ghost_check.ads:9:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:17:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:17:25: "PGI" declared at bad_ancestor.ads:8 with
  ghost policy "Ignore"
bad_extension_ghost_check.ads:17:25: overridden at line 17 with Ghost policy
  "Check"
bad_extension_ghost_check.ads:23:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:23:25: "P" declared at bad_ancestor.ads:4 as
  non-ghost subprogram
bad_extension_ghost_check.ads:23:25: overridden at line 23 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:23:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:23:34: "E3" declared with ghost policy "Check"
bad_extension_ghost_check.ads:23:34: "E3" used at line 23 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:24:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:24:25: "PGC" declared at bad_ancestor.ads:6 with
  ghost policy "Check"
bad_extension_ghost_check.ads:24:25: overridden at line 24 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:24:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:24:34: "E3" declared with ghost policy "Check"
bad_extension_ghost_check.ads:24:34: "E3" used at line 24 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:25:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:25:25: tagged type "E3" declared at line 20 with
  ghost policy "Check"
bad_extension_ghost_check.ads:25:25: primitive subprogram "PGI" declared at
  line 25 with ghost policy "Ignore"
bad_extension_ghost_check.ads:25:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:25:34: "E3" declared with ghost policy "Check"
bad_extension_ghost_check.ads:25:34: "E3" used at line 25 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:30:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:31:25: incompatible overriding in effect
bad_extension_ghost_check.ads:31:25: "PGC" declared at bad_ancestor.ads:15 as
  ghost subprogram
bad_extension_ghost_check.ads:31:25: overridden at line 31 with non-ghost
  subprogram
bad_extension_ghost_check.ads:31:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:32:15: subprogram "PGI" is not overriding
bad_extension_ghost_check.ads:32:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:40:15: subprogram "PGI" is not overriding
bad_extension_ghost_check.ads:46:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:46:25: "P" declared at bad_ancestor.ads:13 as
  non-ghost subprogram
bad_extension_ghost_check.ads:46:25: overridden at line 46 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:46:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:46:34: "E3GC" declared with ghost policy "Check"
bad_extension_ghost_check.ads:46:34: "E3GC" used at line 46 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:47:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:47:25: "PGC" declared at bad_ancestor.ads:15 with
  ghost policy "Check"
bad_extension_ghost_check.ads:47:25: overridden at line 47 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:47:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:47:34: "E3GC" declared with ghost policy "Check"
bad_extension_ghost_check.ads:47:34: "E3GC" used at line 47 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:48:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:48:25: tagged type "E3GC" declared at line 43
  with ghost policy "Check"
bad_extension_ghost_check.ads:48:25: primitive subprogram "PGI" declared at
  line 48 with ghost policy "Ignore"
bad_extension_ghost_check.ads:48:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:48:34: "E3GC" declared with ghost policy "Check"
bad_extension_ghost_check.ads:48:34: "E3GC" used at line 48 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:51:21: incompatible ghost policies in effect
bad_extension_ghost_check.ads:51:21: "RGI" declared with ghost policy "Ignore"
bad_extension_ghost_check.ads:51:21: "RGI" used at line 51 with ghost policy
  "Check"
bad_extension_ghost_check.ads:53:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:54:15: subprogram "PGC" is not overriding
bad_extension_ghost_check.ads:54:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:55:25: incompatible overriding in effect
bad_extension_ghost_check.ads:55:25: "PGI" declared at bad_ancestor.ads:26 as
  ghost subprogram
bad_extension_ghost_check.ads:55:25: overridden at line 55 with non-ghost
  subprogram
bad_extension_ghost_check.ads:55:34: ghost entity cannot appear in this context
bad_extension_ghost_check.ads:58:21: incompatible ghost policies in effect
bad_extension_ghost_check.ads:58:21: "RGI" declared with ghost policy "Ignore"
bad_extension_ghost_check.ads:58:21: "RGI" used at line 58 with ghost policy
  "Check"
bad_extension_ghost_check.ads:62:15: subprogram "PGC" is not overriding
bad_extension_ghost_check.ads:63:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:63:25: "PGI" declared at bad_ancestor.ads:26 with
  ghost policy "Ignore"
bad_extension_ghost_check.ads:63:25: overridden at line 63 with Ghost policy
  "Check"
bad_extension_ghost_check.ads:66:21: incompatible ghost policies in effect
bad_extension_ghost_check.ads:66:21: "RGI" declared with ghost policy "Ignore"
bad_extension_ghost_check.ads:66:21: "RGI" used at line 66 with ghost policy
  "Check"
bad_extension_ghost_check.ads:69:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:69:25: "P" declared at bad_ancestor.ads:22 as
  non-ghost subprogram
bad_extension_ghost_check.ads:69:25: overridden at line 69 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:69:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:69:34: "E3GI" declared with ghost policy "Check"
bad_extension_ghost_check.ads:69:34: "E3GI" used at line 69 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:70:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:70:25: tagged type "E3GI" declared at line 66
  with ghost policy "Check"
bad_extension_ghost_check.ads:70:25: primitive subprogram "PGC" declared at
  line 70 with ghost policy "Ignore"
bad_extension_ghost_check.ads:70:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:70:34: "E3GI" declared with ghost policy "Check"
bad_extension_ghost_check.ads:70:34: "E3GI" used at line 70 with ghost policy
  "Ignore"
bad_extension_ghost_check.ads:71:25: incompatible ghost policies in effect
bad_extension_ghost_check.ads:71:25: tagged type "E3GI" declared at line 66
  with ghost policy "Check"
bad_extension_ghost_check.ads:71:25: primitive subprogram "PGI" declared at
  line 71 with ghost policy "Ignore"
bad_extension_ghost_check.ads:71:34: incompatible ghost policies in effect
bad_extension_ghost_check.ads:71:34: "E3GI" declared with ghost policy "Check"
bad_extension_ghost_check.ads:71:34: "E3GI" used at line 71 with ghost policy
  "Ignore"
bad_ancestor.ads:13:23: ghost entity cannot appear in this context
bad_ancestor.ads:17:14: incompatible ghost policies in effect
bad_ancestor.ads:17:14: tagged type "RGC" declared at line 11 with ghost policy
  "Check"
bad_ancestor.ads:17:14: primitive subprogram "PGI" declared at line 17 with
  ghost policy "Ignore"
bad_ancestor.ads:17:23: incompatible ghost policies in effect
bad_ancestor.ads:17:23: "RGC" declared with ghost policy "Check"
bad_ancestor.ads:17:23: "RGC" used at line 17 with ghost policy "Ignore"
bad_ancestor.ads:22:23: ghost entity cannot appear in this context
bad_ancestor.ads:24:14: incompatible ghost policies in effect
bad_ancestor.ads:24:14: tagged type "RGI" declared at line 20 with ghost policy
  "Ignore"
bad_ancestor.ads:24:14: primitive subprogram "PGC" declared at line 24 with
  ghost policy "Check"
bad_ancestor.ads:24:23: incompatible ghost policies in effect
bad_ancestor.ads:24:23: "RGI" declared with ghost policy "Ignore"
bad_ancestor.ads:24:23: "RGI" used at line 24 with ghost policy "Check"
bad_extension_ghost_ignore.ads:7:34: ghost entity cannot appear in this context
bad_extension_ghost_ignore.ads:8:25: incompatible overriding in effect
bad_extension_ghost_ignore.ads:8:25: "PGC" declared at bad_ancestor.ads:6 as
  ghost subprogram
bad_extension_ghost_ignore.ads:8:25: overridden at line 8 with non-ghost
  subprogram
bad_extension_ghost_ignore.ads:8:34: ghost entity cannot appear in this context
bad_extension_ghost_ignore.ads:9:25: incompatible overriding in effect
bad_extension_ghost_ignore.ads:9:25: "PGI" declared at bad_ancestor.ads:8 as
  ghost subprogram
bad_extension_ghost_ignore.ads:9:25: overridden at line 9 with non-ghost
  subprogram
bad_extension_ghost_ignore.ads:9:34: ghost entity cannot appear in this context
bad_extension_ghost_ignore.ads:15:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:15:25: tagged type "E2" declared at line 12 with
  ghost policy "Ignore"
bad_extension_ghost_ignore.ads:15:25: primitive subprogram "P" declared at line
  15 with ghost policy "Check"
bad_extension_ghost_ignore.ads:15:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:15:34: "E2" declared with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:15:34: "E2" used at line 15 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:16:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:16:25: tagged type "E2" declared at line 12 with
  ghost policy "Ignore"
bad_extension_ghost_ignore.ads:16:25: primitive subprogram "PGC" declared at
  line 16 with ghost policy "Check"
bad_extension_ghost_ignore.ads:16:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:16:34: "E2" declared with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:16:34: "E2" used at line 16 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:17:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:17:25: tagged type "E2" declared at line 12 with
  ghost policy "Ignore"
bad_extension_ghost_ignore.ads:17:25: primitive subprogram "PGI" declared at
  line 17 with ghost policy "Check"
bad_extension_ghost_ignore.ads:17:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:17:34: "E2" declared with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:17:34: "E2" used at line 17 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:28:21: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:28:21: "RGC" declared with ghost policy "Check"
bad_extension_ghost_ignore.ads:28:21: "RGC" used at line 28 with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:30:34: ghost entity cannot appear in this
  context
bad_extension_ghost_ignore.ads:31:25: incompatible overriding in effect
bad_extension_ghost_ignore.ads:31:25: "PGC" declared at bad_ancestor.ads:15 as
  ghost subprogram
bad_extension_ghost_ignore.ads:31:25: overridden at line 31 with non-ghost
  subprogram
bad_extension_ghost_ignore.ads:31:34: ghost entity cannot appear in this
  context
bad_extension_ghost_ignore.ads:32:15: subprogram "PGI" is not overriding
bad_extension_ghost_ignore.ads:32:34: ghost entity cannot appear in this
  context
bad_extension_ghost_ignore.ads:35:21: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:35:21: "RGC" declared with ghost policy "Check"
bad_extension_ghost_ignore.ads:35:21: "RGC" used at line 35 with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:38:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:38:25: tagged type "E2GC" declared at line 35
  with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:38:25: primitive subprogram "P" declared at line
  38 with ghost policy "Check"
bad_extension_ghost_ignore.ads:38:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:38:34: "E2GC" declared with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:38:34: "E2GC" used at line 38 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:39:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:39:25: tagged type "E2GC" declared at line 35
  with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:39:25: primitive subprogram "PGC" declared at
  line 39 with ghost policy "Check"
bad_extension_ghost_ignore.ads:39:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:39:34: "E2GC" declared with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:39:34: "E2GC" used at line 39 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:40:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:40:25: tagged type "E2GC" declared at line 35
  with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:40:25: primitive subprogram "PGI" declared at
  line 40 with ghost policy "Check"
bad_extension_ghost_ignore.ads:40:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:40:34: "E2GC" declared with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:40:34: "E2GC" used at line 40 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:43:21: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:43:21: "RGC" declared with ghost policy "Check"
bad_extension_ghost_ignore.ads:43:21: "RGC" used at line 43 with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:48:15: subprogram "PGI" is not overriding
bad_extension_ghost_ignore.ads:53:34: ghost entity cannot appear in this
  context
bad_extension_ghost_ignore.ads:54:15: subprogram "PGC" is not overriding
bad_extension_ghost_ignore.ads:54:34: ghost entity cannot appear in this
  context
bad_extension_ghost_ignore.ads:55:25: incompatible overriding in effect
bad_extension_ghost_ignore.ads:55:25: "PGI" declared at bad_ancestor.ads:26 as
  ghost subprogram
bad_extension_ghost_ignore.ads:55:25: overridden at line 55 with non-ghost
  subprogram
bad_extension_ghost_ignore.ads:55:34: ghost entity cannot appear in this
  context
bad_extension_ghost_ignore.ads:61:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:61:25: tagged type "E2GI" declared at line 58
  with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:61:25: primitive subprogram "P" declared at line
  61 with ghost policy "Check"
bad_extension_ghost_ignore.ads:61:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:61:34: "E2GI" declared with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:61:34: "E2GI" used at line 61 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:62:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:62:25: tagged type "E2GI" declared at line 58
  with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:62:25: primitive subprogram "PGC" declared at
  line 62 with ghost policy "Check"
bad_extension_ghost_ignore.ads:62:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:62:34: "E2GI" declared with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:62:34: "E2GI" used at line 62 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:63:25: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:63:25: tagged type "E2GI" declared at line 58
  with ghost policy "Ignore"
bad_extension_ghost_ignore.ads:63:25: primitive subprogram "PGI" declared at
  line 63 with ghost policy "Check"
bad_extension_ghost_ignore.ads:63:34: incompatible ghost policies in effect
bad_extension_ghost_ignore.ads:63:34: "E2GI" declared with ghost policy
  "Ignore"
bad_extension_ghost_ignore.ads:63:34: "E2GI" used at line 63 with ghost policy
  "Check"
bad_extension_ghost_ignore.ads:70:15: subprogram "PGC" is not overriding
bad_ancestor.ads:13:23: ghost entity cannot appear in this context
bad_ancestor.ads:17:14: incompatible ghost policies in effect
bad_ancestor.ads:17:14: tagged type "RGC" declared at line 11 with ghost policy
  "Check"
bad_ancestor.ads:17:14: primitive subprogram "PGI" declared at line 17 with
  ghost policy "Ignore"
bad_ancestor.ads:17:23: incompatible ghost policies in effect
bad_ancestor.ads:17:23: "RGC" declared with ghost policy "Check"
bad_ancestor.ads:17:23: "RGC" used at line 17 with ghost policy "Ignore"
bad_ancestor.ads:22:23: ghost entity cannot appear in this context
bad_ancestor.ads:24:14: incompatible ghost policies in effect
bad_ancestor.ads:24:14: tagged type "RGI" declared at line 20 with ghost policy
  "Ignore"
bad_ancestor.ads:24:14: primitive subprogram "PGC" declared at line 24 with
  ghost policy "Check"
bad_ancestor.ads:24:23: incompatible ghost policies in effect
bad_ancestor.ads:24:23: "RGI" declared with ghost policy "Ignore"
bad_ancestor.ads:24:23: "RGI" used at line 24 with ghost policy "Check"

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

-------------- next part --------------
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 235111)
+++ sem_ch3.adb	(working copy)
@@ -14649,8 +14649,8 @@
       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 @@
 
          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.
 
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 235114)
+++ sem_prag.adb	(working copy)
@@ -11585,7 +11585,8 @@
 
                   --  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 @@
                   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 @@
                          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 @@
          --  new form syntax.
 
          when Pragma_Check_Policy => Check_Policy : declare
-            Ident : Node_Id;
-            Kind  : Node_Id;
+            Kind : Node_Id;
 
          begin
             GNAT_Pragma;
@@ -12416,30 +12440,7 @@
                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
 
                Set_Next_Pragma (N, Opt.Check_Policy_List);
@@ -15021,14 +15022,6 @@
                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 @@
 
                   --  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 @@
 
                   --  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 @@
                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,52 +25223,12 @@
 
                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(15))
 
-                        --  The Ghost policy in effect at the point of abstract
-                        --  state declaration and constituent must match
-                        --  (SPARK RM 6.9(16)).
+                  Check_Ghost_Refinement
+                    (State, State_Id, Constit, Constit_Id);
 
-                        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;
-
                   --  A synchronized state must be refined by a synchronized
                   --  object or another synchronized state (SPARK RM 9.6).
 
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 235110)
+++ freeze.adb	(working copy)
@@ -3466,8 +3466,8 @@
 
            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 @@
             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);
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 235111)
+++ sem_res.adb	(working copy)
@@ -4528,7 +4528,7 @@
             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)
Index: contracts.adb
===================================================================
--- contracts.adb	(revision 235113)
+++ contracts.adb	(working copy)
@@ -907,13 +907,13 @@
          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.
 
Index: ghost.adb
===================================================================
--- ghost.adb	(revision 235093)
+++ ghost.adb	(working copy)
@@ -36,6 +36,7 @@
 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 @@
 
       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 @@
                   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;
+                  Check_Policies (Prag_Nam);
+                  return True;
 
-                  --  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;
-
                --  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 @@
                   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 @@
 
       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 @@
    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 @@
      (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;
 
-         elsif Is_Ignored_Ghost_Entity (Over_Subp)
-           and then Is_Checked_Ghost_Entity (Subp)
+         --  A non-Ghost primitive of a type extension cannot override an
+         --  inherited Ghost primitive (SPARK RM 6.9(8)).
+
+         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 --
    ------------------
Index: ghost.ads
===================================================================
--- ghost.ads	(revision 235093)
+++ ghost.ads	(working copy)
@@ -45,17 +45,26 @@
    --  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 @@
 
    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.
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 235114)
+++ sem_ch6.adb	(working copy)
@@ -4701,18 +4701,6 @@
          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 @@
                   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 @@
                   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 @@
                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;


More information about the Gcc-patches mailing list