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 <kirtc...@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.
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;
