https://gcc.gnu.org/g:9c79e191c09d9906e795bd532da6c66e11cecc9d
commit r16-3876-g9c79e191c09d9906e795bd532da6c66e11cecc9d Author: Viljar Indus <[email protected]> Date: Tue Sep 2 10:16:37 2025 +0300 ada: Update ghost code SPARK RM rules gcc/ada/ChangeLog: * contracts.adb: Update SPARK RM reference numbers. * freeze.adb: Likewise. * ghost.adb: Likewise. * ghost.ads: Likewise. * sem_ch12.adb: Likewise. * sem_ch3.adb: Likewise. * sem_ch6.adb: Likewise. * sem_prag.adb: Likwise. * sem_res.adb: Likewise. Diff: --- gcc/ada/contracts.adb | 4 ++-- gcc/ada/freeze.adb | 2 +- gcc/ada/ghost.adb | 44 ++++++++++++++++++++++---------------------- gcc/ada/ghost.ads | 10 +++++----- gcc/ada/sem_ch12.adb | 10 +++++----- gcc/ada/sem_ch3.adb | 4 ++-- gcc/ada/sem_ch6.adb | 14 +++++++------- gcc/ada/sem_prag.adb | 18 +++++++++--------- gcc/ada/sem_res.adb | 2 +- 9 files changed, 54 insertions(+), 54 deletions(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index a6862c424165..d87199939837 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -1131,12 +1131,12 @@ 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(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. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 31a583b769e8..9de4fa409c0f 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -4245,7 +4245,7 @@ package body Freeze is <<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 diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb index ef6315a7d3d5..d097c70b707f 100644 --- a/gcc/ada/ghost.adb +++ b/gcc/ada/ghost.adb @@ -226,7 +226,7 @@ package body Ghost is 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 @@ -260,7 +260,7 @@ package body Ghost is 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 @@ -486,8 +486,8 @@ package body Ghost is 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) @@ -500,14 +500,14 @@ package body Ghost is 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 @@ -728,11 +728,11 @@ package body Ghost is 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 @@ -743,7 +743,7 @@ package body Ghost is 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 @@ -863,7 +863,7 @@ package body Ghost is 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 @@ -882,7 +882,7 @@ package body Ghost is -- 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 @@ -965,7 +965,7 @@ package body Ghost is 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); @@ -1210,7 +1210,7 @@ package body Ghost is 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) @@ -1228,7 +1228,7 @@ package body Ghost is 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) @@ -1249,7 +1249,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(19)). + -- if the primitive is ignored Ghost (SPARK RM 6.9(21)). if Is_Ignored_Ghost_Entity (Subp) then @@ -1288,7 +1288,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(19)). + -- overridden operation is ignored Ghost (SPARK RM 6.9(21)). elsif Is_Ignored_Ghost_Entity (Over_Subp) then @@ -1341,7 +1341,7 @@ package body Ghost is 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) @@ -1407,7 +1407,7 @@ package body Ghost is 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) @@ -1466,14 +1466,14 @@ package body Ghost is 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); @@ -2068,7 +2068,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(16)). + -- point of completion must match (SPARK RM 6.9(18)). Check_Ghost_Completion (Prev_Id => Spec_Id, Compl_Id => Body_Id); @@ -2118,7 +2118,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(16)). + -- point of completion must match (SPARK RM 6.9(18)). Check_Ghost_Completion (Prev_Id => Prev_Id, diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads index cc83d678088b..87401c16a66c 100644 --- a/gcc/ada/ghost.ads +++ b/gcc/ada/ghost.ads @@ -59,7 +59,7 @@ package Ghost is (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; @@ -68,7 +68,7 @@ package Ghost is 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. @@ -79,7 +79,7 @@ package Ghost is 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 @@ -126,7 +126,7 @@ package Ghost is (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 @@ -262,7 +262,7 @@ package Ghost is 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. diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 1ba76dc74cee..0f1746f1ac51 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -2946,7 +2946,7 @@ package body Sem_Ch12 is 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, @@ -4099,7 +4099,7 @@ package body Sem_Ch12 is 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 @@ -11704,7 +11704,7 @@ package body Sem_Ch12 is 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, @@ -12023,7 +12023,7 @@ package body Sem_Ch12 is 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 @@ -12530,7 +12530,7 @@ package body Sem_Ch12 is 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, diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 3317fd209816..5978d6779586 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -10217,7 +10217,7 @@ package body Sem_Ch3 is 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. @@ -10541,7 +10541,7 @@ package body Sem_Ch3 is 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 diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 4e5ede6b429e..5e84889e401d 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -11839,7 +11839,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(18)). + -- (SPARK RM 6.9(21)). Check_Ghost_Primitive (S, B_Typ); end if; @@ -11880,7 +11880,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(18)). + -- (SPARK RM 6.9(21)). Check_Ghost_Primitive (S, B_Typ); end if; @@ -11913,7 +11913,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(18)). + -- (SPARK RM 6.9(21)). Check_Ghost_Primitive (S, B_Typ); end if; @@ -12384,7 +12384,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(19)). + -- (SPARK RM 6.9(21)). Check_Ghost_Overriding (S, Overridden_Subp); end if; @@ -12547,7 +12547,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(19)). + -- must match (SPARK RM 6.9(21)). Check_Ghost_Overriding (E, S); end if; @@ -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(19)). + -- must match (SPARK RM 6.9(21)). Check_Ghost_Overriding (S, E); @@ -12917,7 +12917,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(19)). + -- (SPARK RM 6.9(21)). Check_Ghost_Overriding (S, Overridden_Subp); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 9289e02b56ad..9175490eca27 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -13287,7 +13287,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(21)). + -- versa (SPARK RM 6.9(22)). if Ghost_Seen and Synchronous_Seen then SPARK_Msg_N ("synchronized state cannot be ghost", State); @@ -14854,7 +14854,7 @@ package body Sem_Prag is 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 @@ -14864,7 +14864,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(16)). + -- (SPARK RM 6.9(19)). if Ghost_Config.Ghost_Mode > None then Error_Pragma @@ -19238,7 +19238,7 @@ package body Sem_Prag is 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 @@ -19334,7 +19334,7 @@ package body Sem_Prag is 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 @@ -19392,7 +19392,7 @@ package body Sem_Prag is -- 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; @@ -19410,7 +19410,7 @@ package body Sem_Prag is -- 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 @@ -19421,7 +19421,7 @@ package body Sem_Prag is 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 @@ -19451,7 +19451,7 @@ package body Sem_Prag is 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 diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index f02c223809c7..4d467553373d 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -5273,7 +5273,7 @@ package body Sem_Res is 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)
