@@ -1114,7 +1114,7 @@ package body Contracts is
if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
-- A Ghost object cannot be of a type that yields a synchronized
- -- object (SPARK RM 6.9(19)).
+ -- object (SPARK RM 6.9(21)).
if Yields_Synchronized_Object (Obj_Typ) then
Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
@@ -4094,7 +4094,7 @@ package body Freeze is
<<Skip_Packed>>
-- A Ghost type cannot have a component of protected or task type
- -- (SPARK RM 6.9(19)).
+ -- (SPARK RM 6.9(21)).
if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then
Error_Msg_N
@@ -121,7 +121,7 @@ package body Ghost is
null;
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(16)).
elsif Is_Checked_Ghost_Entity (Prev_Id)
and then Policy = Name_Ignore
@@ -173,9 +173,9 @@ package body Ghost is
--
-- * Be subject to pragma Ghost
- function Is_OK_Pragma (Prag : Node_Id) return Boolean;
+ function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean;
-- Determine whether node Prag is a suitable context for a reference
- -- to a Ghost entity. To qualify as such, Prag must either
+ -- to a Ghost entity Id. To qualify as such, Prag must either
--
-- * Be an assertion expression pragma
--
@@ -318,9 +318,11 @@ package body Ghost is
-- Is_OK_Pragma --
------------------
- function Is_OK_Pragma (Prag : Node_Id) return Boolean is
+ function Is_OK_Pragma (Prag : Node_Id; Id : Entity_Id) return Boolean
+ is
procedure Check_Policies (Prag_Nam : Name_Id);
- -- Verify that the Ghost policy in effect is the same as the
+ -- Verify that the Ghost policy in effect at the point of the
+ -- declaration of Ghost entity Id (if present) is the same as the
-- assertion policy for pragma name Prag_Nam. Emit an error if
-- this is not the case.
@@ -330,14 +332,16 @@ package body Ghost is
procedure Check_Policies (Prag_Nam : Name_Id) is
AP : constant Name_Id := Check_Kind (Prag_Nam);
- GP : constant Name_Id := Policy_In_Effect (Name_Ghost);
begin
- -- If the Ghost policy in effect at the point of a Ghost entity
- -- reference is Ignore, then the assertion policy of the pragma
- -- must be Ignore (SPARK RM 6.9(18)).
+ -- If the Ghost policy in effect at the point of the
+ -- declaration of Ghost entity Id is Ignore, then the assertion
+ -- policy of the pragma must be Ignore (SPARK RM 6.9(20)).
- if GP = Name_Ignore and then AP /= Name_Ignore then
+ if Present (Id)
+ and then not Is_Checked_Ghost_Entity (Id)
+ and then AP /= Name_Ignore
+ then
Error_Msg_N
("incompatible ghost policies in effect",
Ghost_Ref);
@@ -388,7 +392,7 @@ package body Ghost is
and then Prag_Id /= Pragma_Predicate
then
-- Ensure that the assertion policy and the Ghost policy are
- -- compatible (SPARK RM 6.9(18)).
+ -- compatible (SPARK RM 6.9(20)).
Check_Policies (Prag_Nam);
return True;
@@ -535,7 +539,7 @@ package body Ghost is
elsif Is_OK_Declaration (Par) then
return True;
- elsif Is_OK_Pragma (Par) then
+ elsif Is_OK_Pragma (Par, Ghost_Id) then
return True;
elsif Is_OK_Statement (Par) then
@@ -576,7 +580,7 @@ package body Ghost is
begin
-- The Ghost policy in effect a the point of declaration and at the
- -- point of use must match (SPARK RM 6.9(13)).
+ -- point of use must match (SPARK RM 6.9(15)).
if Is_Checked_Ghost_Entity (Id)
and then Policy = Name_Ignore
@@ -859,7 +863,7 @@ package body Ghost is
-- 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 the primitive is ignored Ghost (SPARK RM 6.9(19)).
if Is_Ignored_Ghost_Entity (Subp) then
@@ -900,7 +904,7 @@ package body Ghost is
-- 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)).
+ -- overridden operation is ignored Ghost (SPARK RM 6.9(19)).
elsif Is_Ignored_Ghost_Entity (Over_Subp) then
@@ -950,7 +954,7 @@ package body Ghost is
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)).
+ -- operation and a tagged type must match (SPARK RM 6.9(18)).
if Is_Tagged_Type (Typ) then
if Is_Checked_Ghost_Entity (Prim)
@@ -1001,7 +1005,7 @@ package body Ghost is
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)).
+ -- declaration and constituent must match (SPARK RM 6.9(17)).
if Is_Checked_Ghost_Entity (State_Id)
and then Is_Ignored_Ghost_Entity (Constit_Id)
@@ -1062,7 +1066,7 @@ package body Ghost is
Conc_Typ := Typ;
end if;
- -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
+ -- A Ghost type cannot be concurrent (SPARK RM 6.9(21)). Verify this
-- legality rule first to give a finer-grained diagnostic.
if Present (Conc_Typ) then
@@ -1553,7 +1557,7 @@ package body Ghost is
end if;
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(16)).
Check_Ghost_Completion
(Prev_Id => Spec_Id,
@@ -1600,7 +1604,7 @@ package body Ghost is
end if;
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(14)).
+ -- point of completion must match (SPARK RM 6.9(16)).
Check_Ghost_Completion
(Prev_Id => Prev_Id,
@@ -11693,7 +11693,7 @@ package body Sem_Ch6 is
Check_Private_Overriding (B_Typ);
-- The Ghost policy in effect at the point of declaration
-- or a tagged type and a primitive operation must match
- -- (SPARK RM 6.9(16)).
+ -- (SPARK RM 6.9(18)).
Check_Ghost_Primitive (S, B_Typ);
end if;
@@ -11737,7 +11737,7 @@ package body Sem_Ch6 is
-- 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)).
+ -- (SPARK RM 6.9(18)).
Check_Ghost_Primitive (S, B_Typ);
end if;
@@ -11770,7 +11770,7 @@ package body Sem_Ch6 is
-- 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)).
+ -- (SPARK RM 6.9(18)).
Check_Ghost_Primitive (S, B_Typ);
end if;
@@ -12226,7 +12226,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration of a
-- parent subprogram and an overriding subprogram must match
- -- (SPARK RM 6.9(17)).
+ -- (SPARK RM 6.9(19)).
Check_Ghost_Overriding (S, Overridden_Subp);
end if;
@@ -12389,7 +12389,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration
-- of a parent subprogram and an overriding subprogram
- -- must match (SPARK RM 6.9(17)).
+ -- must match (SPARK RM 6.9(19)).
Check_Ghost_Overriding (E, S);
end if;
@@ -12598,7 +12598,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration
-- of a parent subprogram and an overriding subprogram
- -- must match (SPARK RM 6.9(17)).
+ -- must match (SPARK RM 6.9(19)).
Check_Ghost_Overriding (S, E);
@@ -12751,7 +12751,7 @@ package body Sem_Ch6 is
-- The Ghost policy in effect at the point of declaration of a parent
-- subprogram and an overriding subprogram must match
- -- (SPARK RM 6.9(17)).
+ -- (SPARK RM 6.9(19)).
Check_Ghost_Overriding (S, Overridden_Subp);
@@ -12511,7 +12511,7 @@ package body Sem_Prag is
procedure Check_Ghost_Synchronous is
begin
-- A synchronized abstract state cannot be Ghost and vice
- -- versa (SPARK RM 6.9(19)).
+ -- versa (SPARK RM 6.9(21)).
if Ghost_Seen and Synchronous_Seen then
SPARK_Msg_N ("synchronized state cannot be ghost", State);
@@ -13883,7 +13883,7 @@ package body Sem_Prag is
-- Pragma Assertion_Policy specifying a Ghost policy
-- cannot occur within a Ghost subprogram or package
- -- (SPARK RM 6.9(14)).
+ -- (SPARK RM 6.9(16)).
if Ghost_Mode > None then
Error_Pragma
@@ -17673,7 +17673,7 @@ package body Sem_Prag is
end if;
-- Task unit declared without a definition cannot be subject to
- -- pragma Ghost (SPARK RM 6.9(19)).
+ -- pragma Ghost (SPARK RM 6.9(21)).
elsif Nkind (Stmt) in
N_Single_Task_Declaration | N_Task_Type_Declaration
@@ -17769,7 +17769,7 @@ package body Sem_Prag is
end if;
-- Protected and task types cannot be subject to pragma Ghost
- -- (SPARK RM 6.9(19)).
+ -- (SPARK RM 6.9(21)).
if Nkind (Context) in N_Protected_Body | N_Protected_Definition
then
@@ -17856,7 +17856,7 @@ package body Sem_Prag is
end if;
-- A synchronized object cannot be subject to pragma Ghost
- -- (SPARK RM 6.9(19)).
+ -- (SPARK RM 6.9(21)).
elsif Ekind (Id) = E_Variable then
if Is_Protected_Type (Etype (Id)) then
@@ -29787,7 +29787,7 @@ package body Sem_Prag is
begin
-- The Ghost policy in effect at the point of abstract state
- -- declaration and constituent must match (SPARK RM 6.9(15))
+ -- declaration and constituent must match (SPARK RM 6.9(17))
Check_Ghost_Refinement
(State, State_Id, Constit, Constit_Id);
From: Yannick Moy <moy@adacore.com> Update checking of ghost code after a small change in SPARK RM rules 6.9(15) and 6.9(20), so that the Ghost assertion policy that matters when checking the validity of a reference to a ghost entity in an assertion expression is the Ghost assertion policy at the point of declaration of the entity. Also fix references to SPARK RM rules in comments, which were off by two in many cases after the insertion of rules 13 and 14 regarding generic instantiations. gcc/ada/ * contracts.adb: Fix references to SPARK RM rules. * freeze.adb: Same. * ghost.adb: Fix references to SPARK RM rules. (Check_Ghost_Context): Update checking of references to ghost entities in assertion expressions. * sem_ch6.adb: Fix references to SPARK RM rules. * sem_prag.adb: Same. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/contracts.adb | 2 +- gcc/ada/freeze.adb | 2 +- gcc/ada/ghost.adb | 44 +++++++++++++++++++++++-------------------- gcc/ada/sem_ch6.adb | 14 +++++++------- gcc/ada/sem_prag.adb | 12 ++++++------ 5 files changed, 39 insertions(+), 35 deletions(-)