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
--
-- * 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
--
-- 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.
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);
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;
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
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
-- 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
-- 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
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)
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)
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
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,
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,
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;
-- 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;
-- 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;
-- 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;
-- 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;
-- 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);
-- 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);
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);
-- 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
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
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
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
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);
projects / thirdparty / gcc.git / commitdiff
