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(21)).
+ -- object (SPARK RM 6.9(22)).
if Yields_Synchronized_Object (Obj_Typ) then
Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
- -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)).
+ -- A Ghost object cannot be imported or exported (SPARK RM 6.9(9)).
-- One exception to this is the object that represents the dispatch
-- table of a Ghost tagged type, as the symbol needs to be exported.
<<Skip_Packed>>
-- A Ghost type cannot have a component of protected or task type
- -- (SPARK RM 6.9(21)).
+ -- (SPARK RM 6.9(22)).
if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then
Error_Msg_N
Policy := Ghost_Policy_In_Effect (Prev_Id);
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(16)).
+ -- point of completion must match (SPARK RM 6.9(19)).
if Is_Checked_Ghost_Entity (Prev_Id)
and then Policy = Name_Ignore
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 (SPARK RM 6.9(10)).
+ -- a Ghost entity can safely reside (SPARK RM 6.9(13)).
function In_Aspect_Or_Pragma_Predicate (N : Node_Id) return Boolean;
-- Return True iff N is enclosed in an aspect or pragma Predicate
return True;
-- An assertion expression pragma is Ghost when it contains a
- -- reference to a Ghost entity (SPARK RM 6.9(10)), except for
- -- predicate pragmas (SPARK RM 6.9(11)).
+ -- reference to a Ghost entity (SPARK RM 6.9(13)), except for
+ -- predicate pragmas (SPARK RM 6.9(14)).
elsif Is_Valid_Assertion_Kind (Prag_Nam)
and then Assertion_Expression_Pragma (Prag_Id)
return True;
-- A pragma that applies to a Ghost construct or specifies an
- -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(3))
+ -- aspect of a Ghost entity is a Ghost pragma (SPARK RM 6.9(4))
elsif Is_Ghost_Pragma (Prag) then
return True;
-- Several pragmas that may apply to a non-Ghost entity are
-- treated as Ghost when they contain a reference to a Ghost
- -- entity (SPARK RM 6.9(11)).
+ -- entity (SPARK RM 6.9(18)).
elsif Prag_Nam
in Name_Global
return True;
-- A reference to a Ghost entity can appear within an aspect
- -- specification (SPARK RM 6.9(10)). The precise checking will
+ -- specification (SPARK RM 6.9(13)). The precise checking will
-- occur when analyzing the corresponding pragma. We make an
-- exception for predicate aspects other than Ghost_Predicate
-- that only allow referencing a Ghost entity when the
- -- corresponding type declaration is Ghost (SPARK RM 6.9(11)).
+ -- corresponding type declaration is Ghost (SPARK RM 6.9(14)).
elsif Nkind (Par) = N_Aspect_Specification
and then
return True;
-- A Ghost type may be referenced in a use or use_type clause
- -- (SPARK RM 6.9(10)).
+ -- (SPARK RM 6.9(13)).
elsif Present (Parent (Par))
and then Nkind (Parent (Par)) in N_Use_Package_Clause
end if;
-- The Ghost policy in effect a the point of declaration and at the
- -- point of use must match (SPARK RM 6.9(15)).
+ -- point of use must match (SPARK RM 6.9(18)).
if Is_Checked_Ghost_Entity (Id)
and then Applic_Policy = Ignore
-- assertion-level-dependent on E except in the following cases the
-- specified aspect is either Global, Depends, Refined_Global,
-- Refined_Depends, Initializes, Refined_State, or Iterable (SPARK RM
- -- 6.9(15)).
+ -- 6.9(14)).
if No (Ghost_Region)
or else (Nkind (Ghost_Region) = N_Pragma
end if;
-- If the Ghost entity appears in a non-Ghost context and affects
- -- its behavior or value (SPARK RM 6.9(10,11)).
+ -- its behavior or value (SPARK RM 6.9(13,14)).
if not Is_OK_Ghost_Context (Ghost_Ref) then
Error_Msg_N ("ghost entity cannot appear in this context", Ghost_Ref);
Deriv_Typ := Find_Dispatching_Type (Subp);
-- A Ghost primitive of a non-Ghost type extension cannot override an
- -- inherited non-Ghost primitive (SPARK RM 6.9(8)).
+ -- inherited non-Ghost primitive (SPARK RM 6.9(10)).
if Is_Ghost_Entity (Subp)
and then Present (Deriv_Typ)
end if;
-- A non-Ghost primitive of a type extension cannot override an
- -- inherited Ghost primitive (SPARK RM 6.9(8)).
+ -- inherited Ghost primitive (SPARK RM 6.9(10)).
if Is_Ghost_Entity (Over_Subp)
and then not Is_Ghost_Entity (Subp)
-- 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(19)).
+ -- if the primitive is ignored Ghost (SPARK RM 6.9(21)).
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(19)).
+ -- overridden operation is ignored Ghost (SPARK RM 6.9(21)).
elsif Is_Ignored_Ghost_Entity (Over_Subp) then
end if;
-- The Ghost policy in effect at the point of declaration of a primitive
- -- operation and a tagged type must match (SPARK RM 6.9(20)).
+ -- operation and a tagged type must match (SPARK RM 6.9(21)).
if Is_Checked_Ghost_Entity (Prim)
and then Is_Ignored_Ghost_Entity (Typ)
end if;
-- The Ghost policy in effect at the point of an ignored abstract state
- -- cannot be check (SPARK RM 6.9(19)).
+ -- cannot be check (SPARK RM 6.9(20)).
if Is_Ignored_Ghost_Entity (State_Id)
and then Is_Checked_Ghost_Entity (Constit_Id)
Conc_Typ := Typ;
end if;
- -- A Ghost type cannot be concurrent (SPARK RM 6.9(21)). Verify this
+ -- A Ghost type cannot be concurrent (SPARK RM 6.9(22)). Verify this
-- legality rule first to give a finer-grained diagnostic.
if Present (Conc_Typ) then
Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ);
end if;
- -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
+ -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(9))
if Is_Effectively_Volatile (Full_Typ) then
Error_Msg_N ("ghost type & cannot be volatile", Full_Typ);
end if;
-- The Ghost policy in effect at the point of declaration and at the
- -- point of completion must match (SPARK RM 6.9(16)).
+ -- point of completion must match (SPARK RM 6.9(18)).
Check_Ghost_Completion (Prev_Id => Spec_Id, Compl_Id => Body_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(16)).
+ -- point of completion must match (SPARK RM 6.9(18)).
Check_Ghost_Completion
(Prev_Id => Prev_Id,
(Actual : Node_Id;
Formal : Entity_Id);
-- Check that if Actual contains references to ghost entities, generic
- -- formal parameter Formal is ghost (SPARK RM 6.9(10)).
+ -- formal parameter Formal is ghost (SPARK RM 6.9(13)).
procedure Check_Ghost_Formal_Procedure_Or_Package
(N : Node_Id;
Is_Default : Boolean := False);
-- Verify that if generic formal procedure (resp. package) Formal is ghost,
-- then Actual is not Empty and also a ghost procedure (resp. package)
- -- (SPARK RM 6.9(13-14)). The error if any is located on N. If
+ -- (SPARK RM 6.9(16-17)). The error if any is located on N. If
-- Is_Default is False, N and Actual represent the actual parameter in an
-- instantiation. Otherwise, they represent the default subprogram of a
-- formal subprogram declaration.
Is_Default : Boolean := False);
-- Verify that if Formal (either an IN OUT generic formal parameter, or an
-- IN generic formal parameter of access-to-variable type) is ghost, then
- -- Actual is a ghost object (SPARK RM 6.9(13-14)). Is_Default is True when
+ -- Actual is a ghost object (SPARK RM 6.9(16-17)). Is_Default is True when
-- Actual is the default expression of the formal object declaration.
procedure Check_Ghost_Overriding
(Self : Entity_Id; Other : Entity_Id) return Boolean;
-- Check that assertion level Self is assertion-level-dependent with Other.
--
- -- According to SPARK RM 6.9(5) this means that
+ -- According to SPARK RM 6.9(6) this means that
-- * Either Self or Other has the default assertion level.
-- * Self either is or depends on Other
-- * Self either is or depends on Static
procedure Remove_Ignored_Ghost_Code;
-- Remove all code marked as ignored Ghost from the trees of all qualifying
- -- units (SPARK RM 6.9(4)).
+ -- units (SPARK RM 6.9(5)).
--
-- WARNING: this is a separate front end pass, care should be taken to keep
-- it optimized.
end case;
-- Check for correct use of Ghost entities in generic
- -- instantiations (SPARK RM 6.9(10)).
+ -- instantiations (SPARK RM 6.9(13)).
Check_Ghost_Context_In_Generic_Association
(Actual => Match,
end if;
-- The default for a ghost generic formal procedure should be a ghost
- -- procedure (SPARK RM 6.9(13)).
+ -- procedure (SPARK RM 6.9(16)).
if Ekind (Nam) = E_Procedure then
declare
Formal_Pack := Defining_Unit_Name (Specification (Analyzed_Formal));
-- The actual for a ghost generic formal package should be a ghost
- -- package (SPARK RM 6.9(14)).
+ -- package (SPARK RM 6.9(16)).
Check_Ghost_Formal_Procedure_Or_Package
(N => Actual,
end if;
-- The actual for a ghost generic formal procedure should be a ghost
- -- procedure (SPARK RM 6.9(14)).
+ -- procedure (SPARK RM 6.9(16)).
if Present (Act_E)
and then Ekind (Act_E) = E_Procedure
end if;
-- The actual for a ghost generic formal IN OUT parameter should be a
- -- ghost object (SPARK RM 6.9(14)).
+ -- ghost object (SPARK RM 6.9(16)).
Check_Ghost_Formal_Variable
(Actual => Actual,
end if;
-- A type extension is automatically Ghost when one of its
- -- progenitors is Ghost (SPARK RM 6.9(9)). This property is
+ -- progenitors is Ghost (SPARK RM 6.9(10)). This property is
-- also inherited when the parent type is Ghost, but this is
-- done in Build_Derived_Type as the mechanism also handles
-- untagged derivations.
end if;
-- A derived type becomes Ghost when its parent type is also Ghost
- -- (SPARK RM 6.9(9)). Note that the Ghost-related attributes are not
+ -- (SPARK RM 6.9(10)). Note that the Ghost-related attributes are not
-- directly inherited because the Ghost policy in effect may differ.
if Is_Ghost_Entity (Parent_Type) then
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(18)).
+ -- (SPARK RM 6.9(21)).
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(18)).
+ -- (SPARK RM 6.9(21)).
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(18)).
+ -- (SPARK RM 6.9(21)).
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(19)).
+ -- (SPARK RM 6.9(21)).
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(19)).
+ -- must match (SPARK RM 6.9(21)).
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(19)).
+ -- must match (SPARK RM 6.9(21)).
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(19)).
+ -- (SPARK RM 6.9(21)).
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(21)).
+ -- versa (SPARK RM 6.9(22)).
if Ghost_Seen and Synchronous_Seen then
SPARK_Msg_N ("synchronized state cannot be ghost", State);
if Kind = Name_Ghost then
-- The Ghost policy must be either Check or Ignore
- -- (SPARK RM 6.9(6)).
+ -- (SPARK RM 6.9(8)).
if Chars (Policy) not in Name_Check | Name_Ignore then
Error_Pragma_Arg
-- Pragma Assertion_Policy specifying a Ghost policy
-- cannot occur within a Ghost subprogram or package
- -- (SPARK RM 6.9(16)).
+ -- (SPARK RM 6.9(19)).
if Ghost_Config.Ghost_Mode > None then
Error_Pragma
end if;
-- Task unit declared without a definition cannot be subject to
- -- pragma Ghost (SPARK RM 6.9(21)).
+ -- pragma Ghost (SPARK RM 6.9(22)).
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(21)).
+ -- (SPARK RM 6.9(22)).
if Nkind (Context) in N_Protected_Body | N_Protected_Definition
then
-- The full declaration of a deferred constant cannot be
-- subject to pragma Ghost unless the deferred declaration
- -- is also Ghost (SPARK RM 6.9(9)).
+ -- is also Ghost (SPARK RM 6.9(11)).
if Ekind (Prev_Id) = E_Constant then
Error_Msg_Name_1 := Pname;
-- The full declaration of a type cannot be subject to
-- pragma Ghost unless the partial view is also Ghost
- -- (SPARK RM 6.9(9)).
+ -- (SPARK RM 6.9(11)).
else
Error_Msg_NE (Fix_Error
end if;
-- A synchronized object cannot be subject to pragma Ghost
- -- (SPARK RM 6.9(21)).
+ -- (SPARK RM 6.9(22)).
elsif Ekind (Id) = E_Variable then
if Is_Protected_Type (Etype (Id)) then
Is_Ghost := False;
-- "Ghostness" cannot be turned off once enabled within a
- -- region (SPARK RM 6.9(6)).
+ -- region (SPARK RM 6.9(8)).
if Ghost_Config.Ghost_Mode > None then
Error_Pragma
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(12)).
+ -- mode IN OUT or OUT must be a Ghost variable (SPARK RM 6.9(15)).
if Comes_From_Source (Nam)
and then Is_Ghost_Entity (Nam)
projects / thirdparty / gcc.git / commitdiff
