From c5cec2fe71b243a3a4e76ef41b2ed6b36a3d543c Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Fri, 31 Oct 2014 15:49:31 +0100 Subject: [PATCH] 2014-10-31 Hristian Kirtchev * aspects.adb Add an entry for aspect Ghost in table Canonical_Aspect. * aspects.ads Add an entry for aspect Ghost in tables Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names and Implementation_Defined_Aspect. * einfo.adb: Flags 277 and 278 are now in use. (Is_Checked_Ghost_Entity): New routine. (Is_Ghost_Entity): Removed. (Is_Ghost_Subprogram): Removed. (Is_Ignored_Ghost_Entity): New routine. (Set_Is_Checked_Ghost_Entity): New routine. (Set_Is_Ignored_Ghost_Entity): New routine. (Write_Entity_Flags): Output flags Is_Checked_Ghost_Entity and Is_Ignored_Ghost_Entity. * einfo.ads: Add new flags Is_Checked_Ghost_Entity and Is_Ignored_Ghost_Entity along with usage in nodes. (Is_Checked_Ghost_Entity): New routine and pragma Inline. (Is_Ghost_Entity): Removed along with synthesized flag description and usage in nodes. (Is_Ghost_Subprogram): Removed along with synthesized flag description and usage in nodes. (Is_Ignored_Ghost_Entity): New routine and pragma Inline. (Set_Is_Checked_Ghost_Entity): New routine and pragma Inline. (Set_Is_Ignored_Ghost_Entity): New routine and pragma Inline. * freeze.adb (Freeze_Entity): A Ghost type cannot be effectively volatile. * par-prag.adb Pragma Ghost does not need special handling by the parser. * repinfo.adb (List_Mechanisms): Remove the entry for convention Ghost. * sem_attr.adb (Analyze_Access_Attribute): Remove obsolete check. * sem_ch3.adb (Analyze_Full_Type_Declaration): Mark the type as Ghost when its enclosing context is Ghost. (Analyze_Incomplete_Type_Decl): Mark the type as Ghost when its enclosing context is Ghost. (Analyze_Number_Declaration): Mark the number as Ghost when its enclosing context is Ghost. (Analyze_Object_Declaration): Mark the object as Ghost when its enclosing context is Ghost. Verify the Ghost policy between initial declaration and completion of a deferred constant. (Analyze_Object_Contract): A Ghost variable cannot be effectively volatile, imported or exported. (Build_Derived_Record_Type): Mark a type extension as Ghost when it implements a Ghost interface. (Build_Record_Type): Inherit volatility and "ghostness" from the parent type. (Check_Completion): A Ghost entity declared in a non-Ghost package does not require completion in a body. (Implements_Ghost_Interface): New routine. (Process_Full_View): Inherit "ghostness" from the partial view. Verify the Ghost policy between the partial and full views. Verify the completion of a Ghost type extension. * sem_ch4.adb (Check_Ghost_Subprogram_Call): Removed. * sem_ch5.adb (Analyze_Assignment): Analyze the left hand side first. * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Mark the subprogram as Ghost when its enclosing context is Ghost. (Analyze_Generic_Subprogram_Body): Mark the generic body as Ghost when its enclosing context is Ghost. Verify the Ghost policy between the spec and body. (Analyze_Subprogram_Body_Helper): Mark the body as Ghost when its enclosing context is Ghost. Verify the Ghost policy between the spec and body. (Check_Conformance): A Ghost subprogram profile and a non-Ghost subprogram profile are not subtype conformant. (Convention_Of): Removed. * sem_ch7.adb (Analyze_Package_Body_Helper): Inherit the "ghostness" from the spec. Verify the Ghost policy between the spec and body. (Analyze_Private_Type_Declaration): Mark the type as Ghost when its enclosing context is Ghost. (Requires_Completion_In_Body): New routine. (Unit_Requires_Body): Use Requires_Completion_In_Body. (Unit_Requires_Body_Info): Rename formal parameter P to Pack_Id, update comment on usage and all uses of P in the body. Use Requires_Completion_In_Body. * sem_ch7.ads (Unit_Requires_Body): Rename formal parameter P to Pack_Id, update comment on usage and all uses of P in the body. * sem_ch8.adb (Analyze_Exception_Renaming): Inherit the "ghostness" from the renamed excention. (Analyze_Generic_Renaming): Inherit the "ghostness" from the renamed generic subprogram. (Analyze_Object_Renaming): Inherit the "ghostness" from the renamed object. (Analyze_Package_Renaming): Inherit the "ghostness" from the renamed package. (Analyze_Subprogram_Renaming): Inherit the "ghostness" from the renamed subprogram. * sem_ch11.adb (Analyze_Exception_Declaration): Mark an exception as Ghost when its enclosing context is Ghost. * sem_ch12.adb (Analyze_Generic_Package_Declaration, Analyze_Generic_Subprogram_Declaration): Mark an exception as Ghost when its enclosing context is Ghost. (Preanalyze_Actuals): Remove obsolete check. * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing for aspect Ghost. (Check_Aspect_At_Freeze_Point): Aspects Depends and Global do no need special checking at freeze point. (Insert_After_SPARK_Mode): Update comment on usage. * sem_mech.adb (Set_Mechanisms): Remove the entry for convention Ghost. * sem_prag.adb Add an entry for pragma Ghost in table Sig_Flags. (Analyze_Abstract_State): Update the grammar of the pragma. Add formal parameter Pack_Id along with comment on usage. Mark an abstract state as Ghost when its enclosing context is Ghost. Add processing for option Ghost. (Analyze_Constituent): Verify that a Ghost abstract state is refined by Ghost constituents. (Analyze_Pragma): "Ghost" is now a valid policy. Add checks related to the use and placement of Check_Policy Ghost. Add processing for pragma Ghost. (Check_Ghost_Constituent): New routine. (Is_Valid_Assertion_Kind): "Ghost" is now a valid assertion. (Process_Convention): Remove obsolete check. (Set_Convention_From_Pragma): Remove the processing for convention Ghost. * sem_res.adb (Check_Ghost_Context): New routine. (Resolve_Call): Verify that a reference to a Ghost entity appears in a suitable context. Verify the Ghost polity between point of declaration and point of use. (Resolve_Entity_Name): Verify that a reference to a Ghost entity appears in a suitable context. Verify the Ghost polity between point of declaration and point of use. * sem_util.adb (Check_Ghost_Completion): New routine. (Check_Ghost_Derivation): New routine. (Incomplete_Or_Partial_View): New routine. (Incomplete_Or_Private_View): Removed. (Is_Ghost_Entity): New routine. (Is_Ghost_Statement_Or_Pragma): New routine. (Is_Subject_To_Ghost): New routine. (Policy_In_Effect): New routine. (Set_Is_Ghost_Entity): New routine. (Within_Ghost_Scope): New routine. * sem_util.ads (Check_Ghost_Completion): New routine. (Check_Ghost_Derivation): New routine. (Incomplete_Or_Partial_View): New routine. (Incomplete_Or_Private_View): Removed. (Is_Ghost_Entity): New routine. (Is_Ghost_Statement_Or_Pragma): New routine. (Is_Subject_To_Ghost): New routine. (Policy_In_Effect): New routine. (Set_Is_Ghost_Entity): New routine. (Within_Ghost_Scope): New routine. * snames.adb-tmpl (Get_Convention_Id): Remove the entry for convention Ghost. (Get_Convention_Name): Remove the entry for convention Ghost. * snames.ads-tmpl Remove the convention id for Ghost. Add a pragma id for Ghost. 2014-10-31 Sergey Rybin * gnat_ugn.texi: Add description of --RTS option for ASIS tools. From-SVN: r216981 --- gcc/ada/ChangeLog | 152 ++++++++++++++ gcc/ada/aspects.adb | 1 + gcc/ada/aspects.ads | 5 + gcc/ada/einfo.adb | 83 ++++---- gcc/ada/einfo.ads | 43 ++-- gcc/ada/freeze.adb | 8 + gcc/ada/gnat_ugn.texi | 32 ++- gcc/ada/par-prag.adb | 1 + gcc/ada/repinfo.adb | 2 - gcc/ada/sem_attr.adb | 4 - gcc/ada/sem_ch11.adb | 7 + gcc/ada/sem_ch12.adb | 25 ++- gcc/ada/sem_ch13.adb | 104 +++++++--- gcc/ada/sem_ch3.adb | 214 +++++++++++++++++--- gcc/ada/sem_ch4.adb | 59 ------ gcc/ada/sem_ch5.adb | 6 +- gcc/ada/sem_ch6.adb | 75 ++++--- gcc/ada/sem_ch7.adb | 330 +++++++++++++++--------------- gcc/ada/sem_ch7.ads | 22 +- gcc/ada/sem_ch8.adb | 44 +++- gcc/ada/sem_mech.adb | 1 - gcc/ada/sem_prag.adb | 408 +++++++++++++++++++++++++++++++------ gcc/ada/sem_res.adb | 261 +++++++++++++++++++++--- gcc/ada/sem_util.adb | 432 ++++++++++++++++++++++++++++++++++++++-- gcc/ada/sem_util.ads | 51 ++++- gcc/ada/snames.adb-tmpl | 2 - gcc/ada/snames.ads-tmpl | 6 +- 27 files changed, 1873 insertions(+), 505 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index d8fdff3a68c..1a12ce3f451 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,155 @@ +2014-10-31 Hristian Kirtchev + + * aspects.adb Add an entry for aspect Ghost in table + Canonical_Aspect. + * aspects.ads Add an entry for aspect Ghost in tables + Aspect_Argument, Aspect_Delay, Aspect_Id, Aspect_Names and + Implementation_Defined_Aspect. + * einfo.adb: Flags 277 and 278 are now in use. + (Is_Checked_Ghost_Entity): New routine. + (Is_Ghost_Entity): Removed. + (Is_Ghost_Subprogram): Removed. + (Is_Ignored_Ghost_Entity): New routine. + (Set_Is_Checked_Ghost_Entity): New routine. + (Set_Is_Ignored_Ghost_Entity): New routine. + (Write_Entity_Flags): Output flags Is_Checked_Ghost_Entity and + Is_Ignored_Ghost_Entity. + * einfo.ads: Add new flags Is_Checked_Ghost_Entity + and Is_Ignored_Ghost_Entity along with usage in nodes. + (Is_Checked_Ghost_Entity): New routine and pragma Inline. + (Is_Ghost_Entity): Removed along with synthesized flag + description and usage in nodes. + (Is_Ghost_Subprogram): Removed along with synthesized flag description + and usage in nodes. + (Is_Ignored_Ghost_Entity): New routine and pragma Inline. + (Set_Is_Checked_Ghost_Entity): New routine and pragma Inline. + (Set_Is_Ignored_Ghost_Entity): New routine and pragma Inline. + * freeze.adb (Freeze_Entity): A Ghost type cannot be effectively + volatile. + * par-prag.adb Pragma Ghost does not need special handling by + the parser. + * repinfo.adb (List_Mechanisms): Remove the entry for convention Ghost. + * sem_attr.adb (Analyze_Access_Attribute): Remove obsolete check. + * sem_ch3.adb (Analyze_Full_Type_Declaration): Mark + the type as Ghost when its enclosing context is Ghost. + (Analyze_Incomplete_Type_Decl): Mark the type as Ghost when + its enclosing context is Ghost. + (Analyze_Number_Declaration): Mark the number as Ghost when its + enclosing context is Ghost. + (Analyze_Object_Declaration): Mark the object as Ghost when its + enclosing context is Ghost. Verify the Ghost policy between + initial declaration and completion of a deferred constant. + (Analyze_Object_Contract): A Ghost variable cannot be effectively + volatile, imported or exported. + (Build_Derived_Record_Type): Mark a type extension as Ghost when it + implements a Ghost interface. + (Build_Record_Type): Inherit volatility and "ghostness" from + the parent type. + (Check_Completion): A Ghost entity declared + in a non-Ghost package does not require completion in a body. + (Implements_Ghost_Interface): New routine. + (Process_Full_View): Inherit "ghostness" from the partial view. Verify + the Ghost policy between the partial and full views. Verify the + completion of a Ghost type extension. + * sem_ch4.adb (Check_Ghost_Subprogram_Call): Removed. + * sem_ch5.adb (Analyze_Assignment): Analyze the left hand side first. + * sem_ch6.adb (Analyze_Abstract_Subprogram_Declaration): Mark + the subprogram as Ghost when its enclosing context is Ghost. + (Analyze_Generic_Subprogram_Body): Mark the generic body as Ghost + when its enclosing context is Ghost. Verify the Ghost policy + between the spec and body. + (Analyze_Subprogram_Body_Helper): Mark the body as Ghost when its + enclosing context is Ghost. Verify the Ghost policy between the spec + and body. + (Check_Conformance): A Ghost subprogram profile and a non-Ghost + subprogram profile are not subtype conformant. + (Convention_Of): Removed. + * sem_ch7.adb (Analyze_Package_Body_Helper): Inherit the + "ghostness" from the spec. Verify the Ghost policy between + the spec and body. + (Analyze_Private_Type_Declaration): Mark the type as Ghost when its + enclosing context is Ghost. + (Requires_Completion_In_Body): New routine. + (Unit_Requires_Body): Use Requires_Completion_In_Body. + (Unit_Requires_Body_Info): Rename formal parameter P to Pack_Id, update + comment on usage and all uses of P in the body. Use + Requires_Completion_In_Body. + * sem_ch7.ads (Unit_Requires_Body): Rename formal parameter P + to Pack_Id, update comment on usage and all uses of P in the body. + * sem_ch8.adb (Analyze_Exception_Renaming): Inherit the "ghostness" + from the renamed excention. + (Analyze_Generic_Renaming): Inherit the "ghostness" from the + renamed generic subprogram. + (Analyze_Object_Renaming): Inherit the "ghostness" from the renamed + object. + (Analyze_Package_Renaming): Inherit the "ghostness" from the + renamed package. + (Analyze_Subprogram_Renaming): Inherit the "ghostness" from the + renamed subprogram. + * sem_ch11.adb (Analyze_Exception_Declaration): Mark an exception + as Ghost when its enclosing context is Ghost. + * sem_ch12.adb (Analyze_Generic_Package_Declaration, + Analyze_Generic_Subprogram_Declaration): Mark an exception as + Ghost when its enclosing context is Ghost. + (Preanalyze_Actuals): Remove obsolete check. + * sem_ch13.adb (Analyze_Aspect_Specifications): Add processing + for aspect Ghost. + (Check_Aspect_At_Freeze_Point): Aspects + Depends and Global do no need special checking at freeze point. + (Insert_After_SPARK_Mode): Update comment on usage. + * sem_mech.adb (Set_Mechanisms): Remove the entry for convention Ghost. + * sem_prag.adb Add an entry for pragma Ghost in table Sig_Flags. + (Analyze_Abstract_State): Update the grammar of the pragma. Add + formal parameter Pack_Id along with comment on usage. Mark an + abstract state as Ghost when its enclosing context is Ghost. Add + processing for option Ghost. + (Analyze_Constituent): Verify + that a Ghost abstract state is refined by Ghost constituents. + (Analyze_Pragma): "Ghost" is now a valid policy. Add checks + related to the use and placement of Check_Policy Ghost. Add + processing for pragma Ghost. + (Check_Ghost_Constituent): New routine. + (Is_Valid_Assertion_Kind): "Ghost" is now a valid assertion. + (Process_Convention): Remove obsolete check. + (Set_Convention_From_Pragma): Remove the processing for convention + Ghost. + * sem_res.adb (Check_Ghost_Context): New routine. + (Resolve_Call): Verify that a reference to a Ghost entity appears in a + suitable context. Verify the Ghost polity between point of declaration + and point of use. + (Resolve_Entity_Name): Verify that a reference to + a Ghost entity appears in a suitable context. Verify the Ghost + polity between point of declaration and point of use. + * sem_util.adb (Check_Ghost_Completion): New routine. + (Check_Ghost_Derivation): New routine. + (Incomplete_Or_Partial_View): New routine. + (Incomplete_Or_Private_View): Removed. + (Is_Ghost_Entity): New routine. + (Is_Ghost_Statement_Or_Pragma): New routine. + (Is_Subject_To_Ghost): New routine. + (Policy_In_Effect): New routine. + (Set_Is_Ghost_Entity): New routine. + (Within_Ghost_Scope): New routine. + * sem_util.ads (Check_Ghost_Completion): New routine. + (Check_Ghost_Derivation): New routine. + (Incomplete_Or_Partial_View): New routine. + (Incomplete_Or_Private_View): Removed. + (Is_Ghost_Entity): New routine. + (Is_Ghost_Statement_Or_Pragma): New routine. + (Is_Subject_To_Ghost): New routine. + (Policy_In_Effect): New routine. + (Set_Is_Ghost_Entity): New routine. + (Within_Ghost_Scope): New routine. + * snames.adb-tmpl (Get_Convention_Id): Remove the entry for + convention Ghost. + (Get_Convention_Name): Remove the entry for convention Ghost. + * snames.ads-tmpl Remove the convention id for Ghost. Add a + pragma id for Ghost. + +2014-10-31 Sergey Rybin + + * gnat_ugn.texi: Add description of --RTS option for ASIS tools. + 2014-10-31 Olivier Hainque * gcc-interface/Makefile.in (arm-vxworks): Update target pairs. diff --git a/gcc/ada/aspects.adb b/gcc/ada/aspects.adb index 6e12c3c80e5..19e49b52220 100644 --- a/gcc/ada/aspects.adb +++ b/gcc/ada/aspects.adb @@ -527,6 +527,7 @@ package body Aspects is Aspect_External_Name => Aspect_External_Name, Aspect_External_Tag => Aspect_External_Tag, Aspect_Favor_Top_Level => Aspect_Favor_Top_Level, + Aspect_Ghost => Aspect_Ghost, Aspect_Global => Aspect_Global, Aspect_Implicit_Dereference => Aspect_Implicit_Dereference, Aspect_Import => Aspect_Import, diff --git a/gcc/ada/aspects.ads b/gcc/ada/aspects.ads index 3ca077c986d..0e01beba7a2 100644 --- a/gcc/ada/aspects.ads +++ b/gcc/ada/aspects.ads @@ -98,6 +98,7 @@ package Aspects is Aspect_Extensions_Visible, -- GNAT Aspect_External_Name, Aspect_External_Tag, + Aspect_Ghost, -- GNAT Aspect_Global, -- GNAT Aspect_Implicit_Dereference, Aspect_Initial_Condition, -- GNAT @@ -234,6 +235,7 @@ package Aspects is Aspect_Effective_Writes => True, Aspect_Extensions_Visible => True, Aspect_Favor_Top_Level => True, + Aspect_Ghost => True, Aspect_Global => True, Aspect_Inline_Always => True, Aspect_Invariant => True, @@ -325,6 +327,7 @@ package Aspects is Aspect_Extensions_Visible => Optional_Expression, Aspect_External_Name => Expression, Aspect_External_Tag => Expression, + Aspect_Ghost => Optional_Expression, Aspect_Global => Expression, Aspect_Implicit_Dereference => Name, Aspect_Initial_Condition => Expression, @@ -419,6 +422,7 @@ package Aspects is Aspect_External_Name => Name_External_Name, Aspect_External_Tag => Name_External_Tag, Aspect_Favor_Top_Level => Name_Favor_Top_Level, + Aspect_Ghost => Name_Ghost, Aspect_Global => Name_Global, Aspect_Implicit_Dereference => Name_Implicit_Dereference, Aspect_Import => Name_Import, @@ -698,6 +702,7 @@ package Aspects is Aspect_Effective_Reads => Never_Delay, Aspect_Effective_Writes => Never_Delay, Aspect_Extensions_Visible => Never_Delay, + Aspect_Ghost => Never_Delay, Aspect_Global => Never_Delay, Aspect_Initial_Condition => Never_Delay, Aspect_Initializes => Never_Delay, diff --git a/gcc/ada/einfo.adb b/gcc/ada/einfo.adb index aaa6ea5f060..53ba3db9193 100644 --- a/gcc/ada/einfo.adb +++ b/gcc/ada/einfo.adb @@ -569,15 +569,12 @@ package body Einfo is -- (Has_Protected) Flag271 -- (SSO_Set_Low_By_Default) Flag272 -- (SSO_Set_High_By_Default) Flag273 - -- Is_Generic_Actual_Subprogram Flag274 -- No_Predicate_On_Actual Flag275 -- No_Dynamic_Predicate_On_Actual Flag276 + -- Is_Checked_Ghost_Entity Flag277 + -- Is_Ignored_Ghost_Entity Flag278 - -- (unused) Flag275 - -- (unused) Flag276 - -- (unused) Flag277 - -- (unused) Flag278 -- (unused) Flag279 -- (unused) Flag280 @@ -1926,6 +1923,12 @@ package body Einfo is return Flag63 (Id); end Is_Character_Type; + function Is_Checked_Ghost_Entity (Id : E) return B is + begin + pragma Assert (Nkind (Id) in N_Entity); + return Flag277 (Id); + end Is_Checked_Ghost_Entity; + function Is_Child_Unit (Id : E) return B is begin return Flag73 (Id); @@ -2090,6 +2093,12 @@ package body Einfo is return Flag171 (Id); end Is_Hidden_Open_Scope; + function Is_Ignored_Ghost_Entity (Id : E) return B is + begin + pragma Assert (Nkind (Id) in N_Entity); + return Flag278 (Id); + end Is_Ignored_Ghost_Entity; + function Is_Immediately_Visible (Id : E) return B is begin pragma Assert (Nkind (Id) in N_Entity); @@ -4729,6 +4738,21 @@ package body Einfo is Set_Flag63 (Id, V); end Set_Is_Character_Type; + procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True) is + begin + pragma Assert (Is_Formal (Id) + or else Is_Object (Id) + or else Is_Package_Or_Generic_Package (Id) + or else Is_Subprogram_Or_Generic_Subprogram (Id) + or else Is_Type (Id) + or else Ekind (Id) = E_Abstract_State + or else Ekind (Id) = E_Component + or else Ekind (Id) = E_Discriminant + or else Ekind (Id) = E_Package_Body + or else Ekind (Id) = E_Subprogram_Body); + Set_Flag277 (Id, V); + end Set_Is_Checked_Ghost_Entity; + procedure Set_Is_Child_Unit (Id : E; V : B := True) is begin Set_Flag73 (Id, V); @@ -4871,7 +4895,7 @@ package body Einfo is procedure Set_Is_Generic_Actual_Subprogram (Id : E; V : B := True) is begin - pragma Assert (Ekind (Id) = E_Function or else Ekind (Id) = E_Procedure); + pragma Assert (Ekind_In (Id, E_Function, E_Procedure)); Set_Flag274 (Id, V); end Set_Is_Generic_Actual_Subprogram; @@ -4908,6 +4932,21 @@ package body Einfo is Set_Flag171 (Id, V); end Set_Is_Hidden_Open_Scope; + procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True) is + begin + pragma Assert (Is_Formal (Id) + or else Is_Object (Id) + or else Is_Package_Or_Generic_Package (Id) + or else Is_Subprogram_Or_Generic_Subprogram (Id) + or else Is_Type (Id) + or else Ekind (Id) = E_Abstract_State + or else Ekind (Id) = E_Component + or else Ekind (Id) = E_Discriminant + or else Ekind (Id) = E_Package_Body + or else Ekind (Id) = E_Subprogram_Body); + Set_Flag278 (Id, V); + end Set_Is_Ignored_Ghost_Entity; + procedure Set_Is_Immediately_Visible (Id : E; V : B := True) is begin pragma Assert (Nkind (Id) in N_Entity); @@ -7156,36 +7195,6 @@ package body Einfo is return Ekind (Id) = E_Procedure and then Chars (Id) = Name_uFinalizer; end Is_Finalizer; - --------------------- - -- Is_Ghost_Entity -- - --------------------- - - -- Note: coding below allows for ghost variables. They are not currently - -- implemented, so we will always get False for variables, but that is - -- expected to change in the future. - - function Is_Ghost_Entity (Id : E) return B is - begin - if Present (Id) and then Ekind (Id) = E_Variable then - return Convention (Id) = Convention_Ghost; - else - return Is_Ghost_Subprogram (Id); - end if; - end Is_Ghost_Entity; - - ------------------------- - -- Is_Ghost_Subprogram -- - ------------------------- - - function Is_Ghost_Subprogram (Id : E) return B is - begin - if Present (Id) and then Ekind_In (Id, E_Function, E_Procedure) then - return Convention (Id) = Convention_Ghost; - else - return False; - end if; - end Is_Ghost_Subprogram; - ------------------- -- Is_Null_State -- ------------------- @@ -8479,6 +8488,7 @@ package body Einfo is W ("Is_CPP_Class", Flag74 (Id)); W ("Is_Called", Flag102 (Id)); W ("Is_Character_Type", Flag63 (Id)); + W ("Is_Checked_Ghost_Entity", Flag277 (Id)); W ("Is_Child_Unit", Flag73 (Id)); W ("Is_Class_Wide_Equivalent_Type", Flag35 (Id)); W ("Is_Compilation_Unit", Flag149 (Id)); @@ -8510,6 +8520,7 @@ package body Einfo is W ("Is_Hidden", Flag57 (Id)); W ("Is_Hidden_Non_Overridden_Subpgm", Flag2 (Id)); W ("Is_Hidden_Open_Scope", Flag171 (Id)); + W ("Is_Ignored_Ghost_Entity", Flag278 (Id)); W ("Is_Immediately_Visible", Flag7 (Id)); W ("Is_Implementation_Defined", Flag254 (Id)); W ("Is_Imported", Flag24 (Id)); diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads index 9c2c53c7858..d20624dd07a 100644 --- a/gcc/ada/einfo.ads +++ b/gcc/ada/einfo.ads @@ -2188,6 +2188,13 @@ package Einfo is -- Defined in all entities. Set for character types and subtypes, -- i.e. enumeration types that have at least one character literal. +-- Is_Checked_Ghost_Entity (Flag277) +-- Applies to all entities. Set for abstract states, [generic] packages, +-- [generic] subprograms, components, discriminants, formal parameters, +-- objects, package bodies, subprogram bodies, and [sub]types subject to +-- pragma Ghost or inherit "ghostness" from an enclosing construct, and +-- subject to Assertion_Policy Ghost => Check. + -- Is_Child_Unit (Flag73) -- Defined in all entities. Set only for defining entities of program -- units that are child units (but False for subunits). @@ -2425,18 +2432,6 @@ package Einfo is -- package, generic function, generic procedure), and False for all -- other entities. --- Is_Ghost_Entity (synthesized) --- Applies to all entities. Yields True for a subprogram or a whole --- object that has convention Ghost. For now only functions can have --- Ghost convention, so this will be false for other than functions, --- but we expect that to change in the future. - --- Is_Ghost_Subprogram (synthesized) --- Applies to all entities. Yields True for a subprogram that has a Ghost --- convention. Note: for now, only ghost functions are allowed, so this --- will always be false for procedures, but that is expected to change in --- the future. - -- Is_Hidden (Flag57) -- Defined in all entities. Set for all entities declared in the -- private part or body of a package. Also marks generic formals of a @@ -2458,6 +2453,13 @@ package Einfo is -- instantiation of a child unit, and whose entities are not visible -- during analysis of the instance. +-- Is_Ignored_Ghost_Entity (Flag278) +-- Applies to all entities. Set for abstract states, [generic] packages, +-- [generic] subprograms, components, discriminants, formal parameters, +-- objects, package bodies, subprogram bodies, and [sub]types subject to +-- pragma Ghost or inherit "ghostness" from an enclosing construct, and +-- subject to Assertion_Policy Ghost => Ignore. + -- Is_Immediately_Visible (Flag7) -- Defined in all entities. Set if entity is immediately visible, i.e. -- is defined in some currently open scope (RM 8.3(4)). @@ -5178,6 +5180,7 @@ package Einfo is -- Is_Bit_Packed_Array (Flag122) (base type only) -- Is_Aliased (Flag15) -- Is_Character_Type (Flag63) + -- Is_Checked_Ghost_Entity (Flag277) -- Is_Child_Unit (Flag73) -- Is_Compilation_Unit (Flag149) -- Is_Completely_Hidden (Flag103) @@ -5194,6 +5197,7 @@ package Einfo is -- Is_Generic_Type (Flag13) -- Is_Hidden (Flag57) -- Is_Hidden_Open_Scope (Flag171) + -- Is_Ignored_Ghost_Entity (Flag278) -- Is_Immediately_Visible (Flag7) -- Is_Implementation_Defined (Flag254) -- Is_Imported (Flag24) @@ -5740,8 +5744,6 @@ package Einfo is -- Address_Clause (synth) -- First_Formal (synth) -- First_Formal_With_Extras (synth) - -- Is_Ghost_Entity (synth) (non-generic case only) - -- Is_Ghost_Subprogram (synth) (non-generic case only) -- Last_Formal (synth) -- Number_Formals (synth) -- Scope_Depth (synth) @@ -6037,8 +6039,6 @@ package Einfo is -- First_Formal (synth) -- First_Formal_With_Extras (synth) -- Is_Finalizer (synth) - -- Is_Ghost_Entity (synth) (non-generic case only) - -- Is_Ghost_Subprogram (synth) (non-generic case only) -- Last_Formal (synth) -- Number_Formals (synth) @@ -6249,7 +6249,6 @@ package Einfo is -- Treat_As_Volatile (Flag41) -- Address_Clause (synth) -- Alignment_Clause (synth) - -- Is_Ghost_Entity (synth) -- Size_Clause (synth) -- E_Void @@ -6704,6 +6703,7 @@ package Einfo is function Is_CPP_Class (Id : E) return B; function Is_Called (Id : E) return B; function Is_Character_Type (Id : E) return B; + function Is_Checked_Ghost_Entity (Id : E) return B; function Is_Child_Unit (Id : E) return B; function Is_Class_Wide_Equivalent_Type (Id : E) return B; function Is_Compilation_Unit (Id : E) return B; @@ -6730,6 +6730,7 @@ package Einfo is function Is_Hidden (Id : E) return B; function Is_Hidden_Non_Overridden_Subpgm (Id : E) return B; function Is_Hidden_Open_Scope (Id : E) return B; + function Is_Ignored_Ghost_Entity (Id : E) return B; function Is_Immediately_Visible (Id : E) return B; function Is_Implementation_Defined (Id : E) return B; function Is_Imported (Id : E) return B; @@ -7012,8 +7013,6 @@ package Einfo is function Is_Dynamic_Scope (Id : E) return B; function Is_External_State (Id : E) return B; function Is_Finalizer (Id : E) return B; - function Is_Ghost_Entity (Id : E) return B; - function Is_Ghost_Subprogram (Id : E) return B; function Is_Null_State (Id : E) return B; function Is_Package_Or_Generic_Package (Id : E) return B; function Is_Packed_Array (Id : E) return B; @@ -7343,6 +7342,7 @@ package Einfo is procedure Set_Is_CPP_Class (Id : E; V : B := True); procedure Set_Is_Called (Id : E; V : B := True); procedure Set_Is_Character_Type (Id : E; V : B := True); + procedure Set_Is_Checked_Ghost_Entity (Id : E; V : B := True); procedure Set_Is_Child_Unit (Id : E; V : B := True); procedure Set_Is_Class_Wide_Equivalent_Type (Id : E; V : B := True); procedure Set_Is_Compilation_Unit (Id : E; V : B := True); @@ -7374,6 +7374,7 @@ package Einfo is procedure Set_Is_Hidden (Id : E; V : B := True); procedure Set_Is_Hidden_Non_Overridden_Subpgm (Id : E; V : B := True); procedure Set_Is_Hidden_Open_Scope (Id : E; V : B := True); + procedure Set_Is_Ignored_Ghost_Entity (Id : E; V : B := True); procedure Set_Is_Immediately_Visible (Id : E; V : B := True); procedure Set_Is_Implementation_Defined (Id : E; V : B := True); procedure Set_Is_Imported (Id : E; V : B := True); @@ -8101,6 +8102,7 @@ package Einfo is pragma Inline (Is_CPP_Class); pragma Inline (Is_Called); pragma Inline (Is_Character_Type); + pragma Inline (Is_Checked_Ghost_Entity); pragma Inline (Is_Child_Unit); pragma Inline (Is_Class_Wide_Equivalent_Type); pragma Inline (Is_Class_Wide_Type); @@ -8149,6 +8151,7 @@ package Einfo is pragma Inline (Is_Hidden); pragma Inline (Is_Hidden_Non_Overridden_Subpgm); pragma Inline (Is_Hidden_Open_Scope); + pragma Inline (Is_Ignored_Ghost_Entity); pragma Inline (Is_Immediately_Visible); pragma Inline (Is_Implementation_Defined); pragma Inline (Is_Imported); @@ -8580,6 +8583,7 @@ package Einfo is pragma Inline (Set_Is_CPP_Class); pragma Inline (Set_Is_Called); pragma Inline (Set_Is_Character_Type); + pragma Inline (Set_Is_Checked_Ghost_Entity); pragma Inline (Set_Is_Child_Unit); pragma Inline (Set_Is_Class_Wide_Equivalent_Type); pragma Inline (Set_Is_Compilation_Unit); @@ -8611,6 +8615,7 @@ package Einfo is pragma Inline (Set_Is_Hidden); pragma Inline (Set_Is_Hidden_Non_Overridden_Subpgm); pragma Inline (Set_Is_Hidden_Open_Scope); + pragma Inline (Set_Is_Ignored_Ghost_Entity); pragma Inline (Set_Is_Immediately_Visible); pragma Inline (Set_Is_Implementation_Defined); pragma Inline (Set_Is_Imported); diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index e20aebb1df2..2079271eae1 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -4815,6 +4815,14 @@ package body Freeze is end if; end; + -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(8)) + + if Is_Ghost_Entity (E) + and then Is_Effectively_Volatile (E) + then + SPARK_Msg_N ("ghost type & cannot be volatile", E); + end if; + -- Deal with special cases of freezing for subtype if E /= Base_Type (E) then diff --git a/gcc/ada/gnat_ugn.texi b/gcc/ada/gnat_ugn.texi index 532a0c111d2..1da339ad38f 100644 --- a/gcc/ada/gnat_ugn.texi +++ b/gcc/ada/gnat_ugn.texi @@ -10942,6 +10942,11 @@ Indicates that external variable @var{name} in the argument project has the value @var{value}. Has no effect if no project is specified as tool argument. +@item --RTS=@var{rts-path} +@cindex @option{--RTS} (@command{gnatelim}) +Specifies the default location of the runtime library. Same meaning as the +equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}). + @item -files=@var{filename} @cindex @option{-files} (@code{gnatelim}) Take the argument source files from the specified file. This file should be an @@ -13998,9 +14003,6 @@ uses the same switches as the GNAT compiler, with the same effects: @item -gnatec=@var{path} @cindex @option{-gnatec} (@command{gnatpp}) -@item --RTS=@var{path} -@cindex @option{--RTS} (@command{gnatpp}) - @end table @node Output File Control @@ -14148,6 +14150,11 @@ Indicates that external variable @var{name} in the argument project has the value @var{value}. Has no effect if no project is specified as tool argument. +@item --RTS=@var{rts-path} +@cindex @option{--RTS} (@command{gnatpp}) +Specifies the default location of the runtime library. Same meaning as the +equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}). + @item --incremental @cindex @option{--incremental} @command{gnatpp} Incremental processing on a per-file basis. Source files are only @@ -14586,6 +14593,10 @@ options: the argument project has the value @var{value}. Has no effect if no project is specified as tool argument. +--RTS=@var{rts-path} -- Specifies the default location of the runtime + library. Same meaning as the equivalent @command{gnatmake} flag + (@pxref{Switches for gnatmake}). + --incremental -- incremental processing on a per-file basis. Source files are only processed if they have been modified, or if files they depend on have been modified. This is similar to the way gnatmake/gprbuild @@ -15939,6 +15950,11 @@ Indicates that external variable @var{name} in the argument project has the value @var{value}. Has no effect if no project is specified as tool argument. +@item --RTS=@var{rts-path} +@cindex @option{--RTS} (@command{gnatmetric}) +Specifies the default location of the runtime library. Same meaning as the +equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}). + @item --subdirs=@var{dir} @cindex @option{--subdirs=@var{dir}} @command{gnatmetric} Use the specified subdirectory of the project objects file (or of the @@ -18763,6 +18779,11 @@ Indicates that external variable @var{name} in the argument project has the value @var{value}. Has no effect if no project is specified as tool argument. +@item --RTS=@var{rts-path} +@cindex @option{--RTS} (@command{gnatstub}) +Specifies the default location of the runtime library. Same meaning as the +equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}). + @item --subunits @cindex @option{--subunits} (@command{gnatstub}) Generate subunits for body stubs. If this switch is specified, @@ -19066,6 +19087,11 @@ Recursively consider all sources from all projects. @cindex @option{-X} (@command{gnattest}) Indicate that external variable @var{name} has the value @var{value}. +@item --RTS=@var{rts-path} +@cindex @option{--RTS} (@command{gnattest}) +Specifies the default location of the runtime library. Same meaning as the +equivalent @command{gnatmake} flag (@pxref{Switches for gnatmake}). + @item -q @cindex @option{-q} (@command{gnattest}) Suppresses noncritical output messages. diff --git a/gcc/ada/par-prag.adb b/gcc/ada/par-prag.adb index 7bf57290ca5..93cbf94cadb 100644 --- a/gcc/ada/par-prag.adb +++ b/gcc/ada/par-prag.adb @@ -1226,6 +1226,7 @@ begin Pragma_Favor_Top_Level | Pragma_Fast_Math | Pragma_Finalize_Storage_Only | + Pragma_Ghost | Pragma_Global | Pragma_Ident | Pragma_Implementation_Defined | diff --git a/gcc/ada/repinfo.adb b/gcc/ada/repinfo.adb index cd76da56959..d6f3dde7349 100644 --- a/gcc/ada/repinfo.adb +++ b/gcc/ada/repinfo.adb @@ -720,8 +720,6 @@ package body Repinfo is Write_Line ("Intrinsic"); when Convention_Entry => Write_Line ("Entry"); - when Convention_Ghost => - Write_Line ("Ghost"); when Convention_Protected => Write_Line ("Protected"); when Convention_Assembler => diff --git a/gcc/ada/sem_attr.adb b/gcc/ada/sem_attr.adb index ced9831a61f..e80531453b7 100644 --- a/gcc/ada/sem_attr.adb +++ b/gcc/ada/sem_attr.adb @@ -773,10 +773,6 @@ package body Sem_Attr is elsif Aname = Name_Unchecked_Access then Error_Attr ("attribute% cannot be applied to a subprogram", P); - - elsif Is_Ghost_Subprogram (Entity (P)) then - Error_Attr_P - ("prefix of % attribute cannot be a ghost subprogram"); end if; -- Issue an error if the prefix denotes an eliminated subprogram diff --git a/gcc/ada/sem_ch11.adb b/gcc/ada/sem_ch11.adb index 45b4a082a47..2e3dbd9fe87 100644 --- a/gcc/ada/sem_ch11.adb +++ b/gcc/ada/sem_ch11.adb @@ -64,6 +64,13 @@ package body Sem_Ch11 is Set_Is_Statically_Allocated (Id); Set_Is_Pure (Id, PF); + -- An exception declared within a Ghost scope is automatically Ghost + -- (SPARK RM 6.9(2)). + + if Within_Ghost_Scope then + Set_Is_Ghost_Entity (Id); + end if; + if Has_Aspects (N) then Analyze_Aspect_Specifications (N, Id); end if; diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index 0cf67c6fad2..f982359c749 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -3380,6 +3380,13 @@ package body Sem_Ch12 is Set_Etype (Id, Standard_Void_Type); Set_Contract (Id, Make_Contract (Sloc (Id))); + -- A generic package declared within a Ghost scope is rendered Ghost + -- (SPARK RM 6.9(2)). + + if Within_Ghost_Scope then + Set_Is_Ghost_Entity (Id); + end if; + -- Analyze aspects now, so that generated pragmas appear in the -- declarations before building and analyzing the generic copy. @@ -3580,6 +3587,13 @@ package body Sem_Ch12 is Set_Etype (Id, Standard_Void_Type); end if; + -- A generic subprogram declared within a Ghost scope is rendered Ghost + -- (SPARK RM 6.9(2)). + + if Within_Ghost_Scope then + Set_Is_Ghost_Entity (Id); + end if; + -- For a library unit, we have reconstructed the entity for the unit, -- and must reset it in the library tables. We also make sure that -- Body_Required is set properly in the original compilation unit node. @@ -13040,16 +13054,7 @@ package body Sem_Ch12 is Analyze (Act); end if; - -- Ensure that a ghost subprogram does not act as generic actual - - if Is_Entity_Name (Act) - and then Is_Ghost_Subprogram (Entity (Act)) - then - Error_Msg_N - ("ghost subprogram & cannot act as generic actual", Act); - Abandon_Instantiation (Act); - - elsif Errs /= Serious_Errors_Detected then + if Errs /= Serious_Errors_Detected then -- Do a minimal analysis of the generic, to prevent spurious -- warnings complaining about the generic being unreferenced, diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 826b3dc18a4..da2d6e34d8d 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -1188,10 +1188,11 @@ package body Sem_Ch13 is (Prag : Node_Id; Ins_Nod : Node_Id; Decls : List_Id); - -- Subsidiary to the analysis of aspects Abstract_State, Initializes, - -- Initial_Condition and Refined_State. Insert node Prag before node - -- Ins_Nod. If Ins_Nod is for pragma SPARK_Mode, then skip SPARK_Mode. - -- Decls is the associated declarative list where Prag is to reside. + -- Subsidiary to the analysis of aspects Abstract_State, Ghost, + -- Initializes, Initial_Condition and Refined_State. Insert node Prag + -- before node Ins_Nod. If Ins_Nod is for pragma SPARK_Mode, then skip + -- SPARK_Mode. Decls is the associated declarative list where Prag is to + -- reside. procedure Insert_Pragma (Prag : Node_Id); -- Subsidiary to the analysis of aspects Attach_Handler, Contract_Cases, @@ -2190,10 +2191,11 @@ package body Sem_Ch13 is end loop; end if; - -- Pragma Abstract_State must be inserted after pragma - -- SPARK_Mode in the tree. This ensures that any error - -- messages dependent on SPARK_Mode will be properly - -- enabled/suppressed. + -- When aspects Abstract_State, Ghost, + -- Initial_Condition and Initializes are out of order, + -- ensure that pragma SPARK_Mode is always at the top + -- of the declarations to properly enabled/suppress + -- errors. Insert_After_SPARK_Mode (Prag => Aitem, @@ -2285,6 +2287,57 @@ package body Sem_Ch13 is Insert_Pragma (Aitem); goto Continue; + -- Aspect Ghost is never delayed because it is equivalent to a + -- source pragma which appears at the top of [generic] package + -- declarations or after an object, a [generic] subprogram, or + -- a type declaration. + + when Aspect_Ghost => Ghost : declare + Decls : List_Id; + + begin + Make_Aitem_Pragma + (Pragma_Argument_Associations => New_List ( + Make_Pragma_Argument_Association (Loc, + Expression => Relocate_Node (Expr))), + Pragma_Name => Name_Ghost); + + Decorate (Aspect, Aitem); + + -- When the aspect applies to a [generic] package, insert + -- the pragma at the top of the visible declarations. This + -- emulates the placement of a source pragma. + + if Nkind_In (N, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Decls := Visible_Declarations (Specification (N)); + + if No (Decls) then + Decls := New_List; + Set_Visible_Declarations (N, Decls); + end if; + + -- When aspects Abstract_State, Ghost, Initial_Condition + -- and Initializes are out of order, ensure that pragma + -- SPARK_Mode is always at the top of the declarations to + -- properly enabled/suppress errors. + + Insert_After_SPARK_Mode + (Prag => Aitem, + Ins_Nod => First (Decls), + Decls => Decls); + + -- Otherwise the context is an object, [generic] subprogram + -- or type declaration. + + else + Insert_Pragma (Aitem); + end if; + + goto Continue; + end Ghost; + -- Global -- Aspect Global is never delayed because it is equivalent to @@ -2346,10 +2399,10 @@ package body Sem_Ch13 is Set_Visible_Declarations (Context, Decls); end if; - -- When aspects Abstract_State, Initial_Condition and - -- Initializes are out of order, ensure that pragma - -- SPARK_Mode is always at the top of the declarative - -- list to properly enable/suppress errors. + -- When aspects Abstract_State, Ghost, Initial_Condition + -- and Initializes are out of order, ensure that pragma + -- SPARK_Mode is always at the top of the declarations to + -- properly enabled/suppress errors. Insert_After_SPARK_Mode (Prag => Aitem, @@ -2404,10 +2457,10 @@ package body Sem_Ch13 is Set_Visible_Declarations (Context, Decls); end if; - -- When aspects Abstract_State, Initial_Condition and - -- Initializes are out of order, ensure that pragma - -- SPARK_Mode is always at the top of the declarative - -- list to properly enable/suppress errors. + -- When aspects Abstract_State, Ghost, Initial_Condition + -- and Initializes are out of order, ensure that pragma + -- SPARK_Mode is always at the top of the declarations to + -- properly enabled/suppress errors. Insert_After_SPARK_Mode (Prag => Aitem, @@ -8715,14 +8768,6 @@ package body Sem_Ch13 is when Aspect_Default_Value => T := Entity (ASN); - -- Depends is a delayed aspect because it mentiones names first - -- introduced by aspect Global which is already delayed. There is - -- no action to be taken with respect to the aspect itself as the - -- analysis is done by the corresponding pragma. - - when Aspect_Depends => - return; - when Aspect_Dispatching_Domain => T := RTE (RE_Dispatching_Domain); @@ -8732,14 +8777,6 @@ package body Sem_Ch13 is when Aspect_External_Name => T := Standard_String; - -- Global is a delayed aspect because it may reference names that - -- have not been declared yet. There is no action to be taken with - -- respect to the aspect itself as the reference checking is done - -- on the corresponding pragma. - - when Aspect_Global => - return; - when Aspect_Link_Name => T := Standard_String; @@ -8847,9 +8884,12 @@ package body Sem_Ch13 is Aspect_Annotate | Aspect_Contract_Cases | Aspect_Default_Initial_Condition | + Aspect_Depends | Aspect_Dimension | Aspect_Dimension_System | Aspect_Extensions_Visible | + Aspect_Ghost | + Aspect_Global | Aspect_Implicit_Dereference | Aspect_Initial_Condition | Aspect_Initializes | diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index 9e79041a302..8579e083313 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -2617,7 +2617,6 @@ package body Sem_Ch3 is Set_Analyzed (T); case Nkind (Def) is - when N_Access_To_Subprogram_Definition => Access_Subprogram_Declaration (T, Def); @@ -2705,13 +2704,20 @@ package body Sem_Ch3 is Check_SPARK_05_Restriction ("controlled type is not allowed", N); end if; + -- A type declared within a Ghost scope is automatically Ghost + -- (SPARK RM 6.9(2)). + + if Comes_From_Source (T) and then Within_Ghost_Scope then + Set_Is_Ghost_Entity (T); + end if; + -- Some common processing for all types Set_Depends_On_Private (T, Has_Private_Component (T)); Check_Ops_From_Incomplete_Type; - -- Both the declared entity, and its anonymous base type if one - -- was created, need freeze nodes allocated. + -- Both the declared entity, and its anonymous base type if one was + -- created, need freeze nodes allocated. declare B : constant Entity_Id := Base_Type (T); @@ -2850,6 +2856,13 @@ package body Sem_Ch3 is Set_Is_First_Subtype (T, True); Set_Etype (T, T); + -- An incomplete type declared within a Ghost scope is automatically + -- Ghost (SPARK RM 6.9(2)). + + if Within_Ghost_Scope then + Set_Is_Ghost_Entity (T); + end if; + -- Ada 2005 (AI-326): Minimum decoration to give support to tagged -- incomplete types. @@ -2960,6 +2973,13 @@ package body Sem_Ch3 is Generate_Definition (Id); Enter_Name (Id); + -- A number declared within a Ghost scope is automatically Ghost + -- (SPARK RM 6.9(2)). + + if Within_Ghost_Scope then + Set_Is_Ghost_Entity (Id); + end if; + -- This is an optimization of a common case of an integer literal if Nkind (E) = N_Integer_Literal then @@ -3099,6 +3119,13 @@ package body Sem_Ch3 is Seen : Boolean := False; begin + -- The loop parameter in an element iterator over a formal container + -- is declared with an object declaration but no contracts apply. + + if Ekind (Obj_Id) = E_Loop_Parameter then + return; + end if; + if Ekind (Obj_Id) = E_Constant then -- A constant cannot be effectively volatile. This check is only @@ -3113,12 +3140,6 @@ package body Sem_Ch3 is Error_Msg_N ("constant cannot be volatile", Obj_Id); end if; - -- The loop parameter in an element iterator over a formal container - -- is declared with an object declaration but no contracts apply. - - elsif Ekind (Obj_Id) = E_Loop_Parameter then - null; - else pragma Assert (Ekind (Obj_Id) = E_Variable); -- The following checks are only relevant when SPARK_Mode is on as @@ -3164,6 +3185,25 @@ package body Sem_Ch3 is Obj_Id); end if; end if; + + if Is_Ghost_Entity (Obj_Id) then + + -- A Ghost object cannot be effectively volatile + -- (SPARK RM 6.9(8)). + + if Is_Effectively_Volatile (Obj_Id) then + SPARK_Msg_N ("ghost variable & cannot be volatile", Obj_Id); + + -- A Ghost object cannot be imported or exported + -- (SPARK RM 6.9(8)). + + elsif Is_Imported (Obj_Id) then + SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id); + + elsif Is_Exported (Obj_Id) then + SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id); + end if; + end if; end if; -- Analyze all external properties @@ -3211,6 +3251,17 @@ package body Sem_Ch3 is Check_Missing_Part_Of (Obj_Id); end if; end if; + + -- A ghost object cannot be imported or exported (SPARK RM 6.9(8)) + + if Is_Ghost_Entity (Obj_Id) then + if Is_Exported (Obj_Id) then + SPARK_Msg_N ("ghost object & cannot be exported", Obj_Id); + + elsif Is_Imported (Obj_Id) then + SPARK_Msg_N ("ghost object & cannot be imported", Obj_Id); + end if; + end if; end Analyze_Object_Contract; -------------------------------- @@ -3522,8 +3573,7 @@ package body Sem_Ch3 is -- and must not be unconstrained. (The only exception to this is the -- acceptance of declarations of constants of type String.) - if not - Nkind_In (Object_Definition (N), N_Identifier, N_Expanded_Name) + if not Nkind_In (Object_Definition (N), N_Expanded_Name, N_Identifier) then Check_SPARK_05_Restriction ("subtype mark required", Object_Definition (N)); @@ -3869,6 +3919,23 @@ package body Sem_Ch3 is Set_Ekind (Id, E_Variable); end if; + -- An object declared within a Ghost scope is automatically + -- Ghost (SPARK RM 6.9(2)). + + if Comes_From_Source (Id) and then Within_Ghost_Scope then + Set_Is_Ghost_Entity (Id); + + -- The Ghost policy in effect at the point of declaration + -- and at the point of completion must match + -- (SPARK RM 6.9(14)). + + if Present (Prev_Entity) + and then Is_Ghost_Entity (Prev_Entity) + then + Check_Ghost_Completion (Prev_Entity, Id); + end if; + end if; + Rewrite (N, Make_Object_Renaming_Declaration (Loc, Defining_Identifier => Id, @@ -3991,7 +4058,7 @@ package body Sem_Ch3 is -- true for variables so far (will be reset for a variable if and when -- we encounter a modification in the source). - Set_Never_Set_In_Source (Id, True); + Set_Never_Set_In_Source (Id); -- Now establish the proper kind and type of the object @@ -4021,7 +4088,7 @@ package body Sem_Ch3 is -- the case of exception choice variables, it will already be true). if Present (E) then - Set_Has_Initial_Value (Id, True); + Set_Has_Initial_Value (Id); end if; Set_Contract (Id, Make_Contract (Sloc (Id))); @@ -4033,6 +4100,27 @@ package body Sem_Ch3 is Init_Esize (Id); Set_Optimize_Alignment_Flags (Id); + -- An object declared within a Ghost scope is automatically Ghost + -- (SPARK RM 6.9(2)). This property is also inherited when its type + -- is Ghost or the previous declaration of the deferred constant is + -- Ghost. + + if Comes_From_Source (Id) + and then (Is_Ghost_Entity (T) + or else (Present (Prev_Entity) + and then Is_Ghost_Entity (Prev_Entity)) + or else Within_Ghost_Scope) + then + Set_Is_Ghost_Entity (Id); + + -- The Ghost policy in effect at the point of declaration and at the + -- point of completion must match (SPARK RM 6.9(14)). + + if Present (Prev_Entity) and then Is_Ghost_Entity (Prev_Entity) then + Check_Ghost_Completion (Prev_Entity, Id); + end if; + end if; + -- Deal with aliased case if Aliased_Present (N) then @@ -7636,6 +7724,34 @@ package body Sem_Ch3 is Derived_Type : Entity_Id; Derive_Subps : Boolean := True) is + function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean; + -- Determine whether type Typ implements at least one Ghost interface + + -------------------------------- + -- Implements_Ghost_Interface -- + -------------------------------- + + function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean is + Iface_Elmt : Elmt_Id; + begin + -- Traverse the list of interfaces looking for a Ghost interface + + if Is_Tagged_Type (Typ) and then Present (Interfaces (Typ)) then + Iface_Elmt := First_Elmt (Interfaces (Typ)); + while Present (Iface_Elmt) loop + if Is_Ghost_Entity (Node (Iface_Elmt)) then + return True; + end if; + + Next_Elmt (Iface_Elmt); + end loop; + end if; + + return False; + end Implements_Ghost_Interface; + + -- Local variables + Discriminant_Specs : constant Boolean := Present (Discriminant_Specifications (N)); Is_Tagged : constant Boolean := Is_Tagged_Type (Parent_Type); @@ -7663,6 +7779,8 @@ package body Sem_Ch3 is -- An empty Discs list means that there were no constraints in the -- subtype indication or that there was an error processing it. + -- Start of processing for Build_Derived_Record_Type + begin if Ekind (Parent_Type) = E_Record_Type_With_Private and then Present (Full_View (Parent_Type)) @@ -8214,7 +8332,7 @@ package body Sem_Ch3 is declare Corr_Disc : constant Entity_Id := - Corresponding_Discriminant (Discrim); + Corresponding_Discriminant (Discrim); Disc_Type : constant Entity_Id := Etype (Discrim); Corr_Type : Entity_Id; @@ -8496,7 +8614,7 @@ package body Sem_Ch3 is if Is_Itype (Derived_Type) then declare Def : constant Node_Id := - Associated_Node_For_Itype (Derived_Type); + Associated_Node_For_Itype (Derived_Type); begin if Present (Def) and then Nkind (Def) = N_Full_Type_Declaration @@ -8506,6 +8624,16 @@ package body Sem_Ch3 is end if; end; end if; + + -- A type extension is automatically Ghost when one of its + -- progenitors is Ghost (SPARK RM 6.9(9)). 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. + + if Implements_Ghost_Interface (Derived_Type) then + Set_Is_Ghost_Entity (Derived_Type); + end if; end; end if; @@ -8700,6 +8828,7 @@ package body Sem_Ch3 is Set_RM_Size (Derived_Type, RM_Size (Parent_Type)); Set_Is_Controlled (Derived_Type, Is_Controlled (Parent_Type)); Set_Is_Tagged_Type (Derived_Type, Is_Tagged_Type (Parent_Type)); + Set_Is_Volatile (Derived_Type, Is_Volatile (Parent_Type)); if Is_Tagged_Type (Derived_Type) then Set_No_Tagged_Streams_Pragma @@ -8716,7 +8845,7 @@ package body Sem_Ch3 is -- type may be set in the private part, and not propagated to the -- subtype until later, so we obtain the convention from the base type. - Set_Convention (Derived_Type, Convention (Parent_Base)); + Set_Convention (Derived_Type, Convention (Parent_Base)); -- Set SSO default for record or array type @@ -8759,6 +8888,13 @@ package body Sem_Ch3 is Set_May_Inherit_Delayed_Rep_Aspects (Derived_Type); end if; + -- Propagate the attributes related to pragma Ghost from the parent type + -- to the derived type or type extension (SPARK RM 6.9(9)). + + if Is_Ghost_Entity (Parent_Type) then + Set_Is_Ghost_Entity (Derived_Type); + end if; + -- Type dependent processing case Ekind (Parent_Type) is @@ -10646,14 +10782,24 @@ package body Sem_Ch3 is end if; end Post_Error; + -- Local variables + + Pack_Id : constant Entity_Id := Current_Scope; + -- Start of processing for Check_Completion begin - E := First_Entity (Current_Scope); + E := First_Entity (Pack_Id); while Present (E) loop if Is_Intrinsic_Subprogram (E) then null; + -- A Ghost entity declared in a non-Ghost package does not force the + -- need for a body (SPARK RM 6.9(11)). + + elsif not Is_Ghost_Entity (Pack_Id) and then Is_Ghost_Entity (E) then + null; + -- The following situation requires special handling: a child unit -- that appears in the context clause of the body of its parent: @@ -10678,10 +10824,10 @@ package body Sem_Ch3 is -- this kind is reserved for predefined operators, that are -- intrinsic and do not need completion. - elsif Ekind_In (E, E_Function, - E_Procedure, - E_Generic_Function, - E_Generic_Procedure) + elsif Ekind_In (E, E_Function, + E_Procedure, + E_Generic_Function, + E_Generic_Procedure) then if Has_Completion (E) then null; @@ -11834,8 +11980,7 @@ package body Sem_Ch3 is then Error_Msg_Sloc := Sloc (Prev); Error_Msg_N - ("full constant for declaration#" - & " must be in private part", N); + ("full constant for declaration # must be in private part", N); elsif Ekind (Current_Scope) = E_Package and then @@ -14581,7 +14726,8 @@ package body Sem_Ch3 is and then Designated_Type (Etype (New_Subp)) = Derived_Type and then not Is_Null_Extension (Derived_Type)) - or else Is_EVF_Procedure (Alias (New_Subp))) + or else (Comes_From_Source (Alias (New_Subp)) + and then Is_EVF_Procedure (Alias (New_Subp)))) and then No (Actual_Subp) then if not Is_Tagged_Type (Derived_Type) @@ -19636,6 +19782,26 @@ package body Sem_Ch3 is Private_To_Full_View => True); end if; + -- Propagate the attributes related to pragma Ghost from the private to + -- the full view. + + if Is_Ghost_Entity (Priv_T) then + Set_Is_Ghost_Entity (Full_T); + + -- The Ghost policy in effect at the point of declaration and at the + -- point of completion must match (SPARK RM 6.9(14)). + + 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; + end if; + -- Propagate invariants to full type if Has_Invariants (Priv_T) then diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index 6f58d001639..0167f90565d 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -854,11 +854,6 @@ package body Sem_Ch4 is -- Flag indicates whether an interpretation of the prefix is a -- parameterless call that returns an access_to_subprogram. - procedure Check_Ghost_Subprogram_Call; - -- Verify the legality of a call to a ghost subprogram. Such calls can - -- appear only in assertion expressions except subtype predicates or - -- from within another ghost subprogram. - procedure Check_Mixed_Parameter_And_Named_Associations; -- Check that parameter and named associations are not mixed. This is -- a restriction in SPARK mode. @@ -873,53 +868,6 @@ package body Sem_Ch4 is procedure No_Interpretation; -- Output error message when no valid interpretation exists - --------------------------------- - -- Check_Ghost_Subprogram_Call -- - --------------------------------- - - procedure Check_Ghost_Subprogram_Call is - S : Entity_Id; - - begin - -- Do not perform the check while preanalyzing the enclosing context - -- because the call is not in its final place. Premature attempts to - -- verify the placement lead to bogus errors. - - if In_Spec_Expression then - return; - - -- The ghost subprogram appears inside an assertion expression which - -- is one of the allowed cases. - - elsif In_Assertion_Expression_Pragma (N) then - return; - - -- Otherwise see if it inside another ghost subprogram - - else - -- Loop to climb scopes - - S := Current_Scope; - while Present (S) and then S /= Standard_Standard loop - - -- The call appears inside another ghost subprogram - - if Is_Ghost_Subprogram (S) then - return; - end if; - - S := Scope (S); - end loop; - - -- If we fall through the loop it was not within another - -- ghost subprogram, so we have bad placement. - - Error_Msg_N - ("call to ghost subprogram must appear in assertion expression " - & "or another ghost subprogram", N); - end if; - end Check_Ghost_Subprogram_Call; - -------------------------------------------------- -- Check_Mixed_Parameter_And_Named_Associations -- -------------------------------------------------- @@ -1308,13 +1256,6 @@ package body Sem_Ch4 is End_Interp_List; end if; - - -- A call to a ghost subprogram is allowed only in assertion expressions - -- excluding subtype predicates or from within another ghost subprogram. - - if Is_Ghost_Subprogram (Get_Subprogram_Entity (N)) then - Check_Ghost_Subprogram_Call; - end if; end Analyze_Call; ----------------------------- diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index 245464a6706..0e09a02acf7 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -273,8 +273,12 @@ package body Sem_Ch5 is begin Mark_Coextensions (N, Rhs); - Analyze (Rhs); + -- Analyze the target of the assignment first in case the expression + -- contains references to Ghost entities. The checks that verify the + -- proper use of a Ghost entity need to know the enclosing context. + Analyze (Lhs); + Analyze (Rhs); -- Ensure that we never do an assignment on a variable marked as -- as Safe_To_Reevaluate. diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 27e2706f927..1ef29c55387 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -223,6 +223,13 @@ package body Sem_Ch6 is Set_Categorization_From_Scope (Designator, Scop); + -- An abstract subprogram declared within a Ghost scope is automatically + -- Ghost (SPARK RM 6.9(2)). + + if Comes_From_Source (Designator) and then Within_Ghost_Scope then + Set_Is_Ghost_Entity (Designator); + end if; + if Ekind (Scope (Designator)) = E_Protected_Type then Error_Msg_N ("abstract subprogram not allowed in protected type", N); @@ -1204,6 +1211,20 @@ package body Sem_Ch6 is Set_Convention (Body_Id, Convention (Gen_Id)); Set_Is_Obsolescent (Body_Id, Is_Obsolescent (Gen_Id)); Set_Scope (Body_Id, Scope (Gen_Id)); + + -- Inherit the "ghostness" of the generic spec. Note that this + -- property is not directly inherited as the body may be subject + -- to a different Ghost assertion policy. + + if Is_Ghost_Entity (Gen_Id) or else Within_Ghost_Scope then + Set_Is_Ghost_Entity (Body_Id); + + -- The Ghost policy in effect at the point of declaration and at + -- the point of completion must match (SPARK RM 6.9(14)). + + Check_Ghost_Completion (Gen_Id, Body_Id); + end if; + Check_Fully_Conformant (Body_Id, Gen_Id, Body_Id); if Nkind (N) = N_Subprogram_Body_Stub then @@ -3309,6 +3330,19 @@ package body Sem_Ch6 is Set_Convention (Body_Id, Convention (Spec_Id)); Set_Has_Completion (Spec_Id); + -- Inherit the "ghostness" of the subprogram spec. Note that this + -- property is not directly inherited as the body may be subject + -- to a different Ghost assertion policy. + + if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then + Set_Is_Ghost_Entity (Body_Id); + + -- The Ghost policy in effect at the point of declaration and + -- at the point of completion must match (SPARK RM 6.9(14)). + + Check_Ghost_Completion (Spec_Id, Body_Id); + end if; + if Is_Protected_Type (Scope (Spec_Id)) then Prot_Typ := Scope (Spec_Id); end if; @@ -4195,6 +4229,13 @@ package body Sem_Ch6 is Set_SPARK_Pragma (Designator, SPARK_Mode_Pragma); Set_SPARK_Pragma_Inherited (Designator, True); + -- A subprogram declared within a Ghost scope is automatically Ghost + -- (SPARK RM 6.9(2)). + + if Comes_From_Source (Designator) and then Within_Ghost_Scope then + Set_Is_Ghost_Entity (Designator); + end if; + if Debug_Flag_C then Write_Str ("==> subprogram spec "); Write_Name (Chars (Designator)); @@ -4640,7 +4681,6 @@ package body Sem_Ch6 is if Old_Type /= Standard_Void_Type and then New_Type /= Standard_Void_Type then - -- If we are checking interface conformance we omit controlling -- arguments and result, because we are only checking the conformance -- of the remaining parameters. @@ -4719,6 +4759,13 @@ package body Sem_Ch6 is 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)). + + elsif Is_Ghost_Entity (Old_Id) /= Is_Ghost_Entity (New_Id) then + Conformance_Error ("\ghost modes do not match!"); + return; end if; end if; @@ -5143,34 +5190,12 @@ package body Sem_Ch6 is ---------------------- procedure Check_Convention (Op : Entity_Id) is - function Convention_Of (Id : Entity_Id) return Convention_Id; - -- Given an entity, return its convention. The function treats Ghost - -- as convention Ada because the two have the same dynamic semantics. - - ------------------- - -- Convention_Of -- - ------------------- - - function Convention_Of (Id : Entity_Id) return Convention_Id is - Conv : constant Convention_Id := Convention (Id); - begin - if Conv = Convention_Ghost then - return Convention_Ada; - else - return Conv; - end if; - end Convention_Of; - - -- Local variables - - Op_Conv : constant Convention_Id := Convention_Of (Op); + Op_Conv : constant Convention_Id := Convention (Op); Iface_Conv : Convention_Id; Iface_Elmt : Elmt_Id; Iface_Prim_Elmt : Elmt_Id; Iface_Prim : Entity_Id; - -- Start of processing for Check_Convention - begin Iface_Elmt := First_Elmt (Ifaces_List); while Present (Iface_Elmt) loop @@ -5178,7 +5203,7 @@ package body Sem_Ch6 is First_Elmt (Primitive_Operations (Node (Iface_Elmt))); while Present (Iface_Prim_Elmt) loop Iface_Prim := Node (Iface_Prim_Elmt); - Iface_Conv := Convention_Of (Iface_Prim); + Iface_Conv := Convention (Iface_Prim); if Is_Interface_Conformant (Typ, Iface_Prim, Op) and then Iface_Conv /= Op_Conv diff --git a/gcc/ada/sem_ch7.adb b/gcc/ada/sem_ch7.adb index f15b8ff547e..b96c27af43e 100644 --- a/gcc/ada/sem_ch7.adb +++ b/gcc/ada/sem_ch7.adb @@ -108,20 +108,6 @@ package body Sem_Ch7 is -- created at the beginning of the corresponding package body and inserted -- before other body declarations. - procedure Install_Package_Entity (Id : Entity_Id); - -- Supporting procedure for Install_{Visible,Private}_Declarations. Places - -- one entity on its visibility chain, and recurses on the visible part if - -- the entity is an inner package. - - function Is_Private_Base_Type (E : Entity_Id) return Boolean; - -- True for a private type that is not a subtype - - function Is_Visible_Dependent (Dep : Entity_Id) return Boolean; - -- If the private dependent is a private type whose full view is derived - -- from the parent type, its full properties are revealed only if we are in - -- the immediate scope of the private dependent. Should this predicate be - -- tightened further??? - procedure Declare_Inherited_Private_Subprograms (Id : Entity_Id); -- Called upon entering the private part of a public child package and the -- body of a nested package, to potentially declare certain inherited @@ -137,10 +123,31 @@ package body Sem_Ch7 is -- inherited private operation has been overridden, then it's replaced by -- the overriding operation. - procedure Unit_Requires_Body_Info (P : Entity_Id); - -- Outputs info messages showing why package specification P requires a - -- body. Caller has checked that the switch requesting this information - -- is set, and that the package does indeed require a body. + procedure Install_Package_Entity (Id : Entity_Id); + -- Supporting procedure for Install_{Visible,Private}_Declarations. Places + -- one entity on its visibility chain, and recurses on the visible part if + -- the entity is an inner package. + + function Is_Private_Base_Type (E : Entity_Id) return Boolean; + -- True for a private type that is not a subtype + + function Is_Visible_Dependent (Dep : Entity_Id) return Boolean; + -- If the private dependent is a private type whose full view is derived + -- from the parent type, its full properties are revealed only if we are in + -- the immediate scope of the private dependent. Should this predicate be + -- tightened further??? + + function Requires_Completion_In_Body + (Id : Entity_Id; + Pack_Id : Entity_Id) return Boolean; + -- Subsidiary to routines Unit_Requires_Body and Unit_Requires_Body_Info. + -- Determine whether entity Id declared in package spec Pack_Id requires + -- completion in a package body. + + procedure Unit_Requires_Body_Info (Pack_Id : Entity_Id); + -- Outputs info messages showing why package Pack_Id requires a body. The + -- caller has checked that the switch requesting this information is set, + -- and that the package does indeed require a body. -------------------------- -- Analyze_Package_Body -- @@ -588,13 +595,14 @@ package body Sem_Ch7 is -- been set. if Present (Corresponding_Spec (N)) then - Spec_Id := Corresponding_Spec (N); + Spec_Id := Corresponding_Spec (N); Pack_Decl := Unit_Declaration_Node (Spec_Id); else Spec_Id := Current_Entity_In_Scope (Defining_Entity (N)); - if Present (Spec_Id) and then Is_Package_Or_Generic_Package (Spec_Id) + if Present (Spec_Id) + and then Is_Package_Or_Generic_Package (Spec_Id) then Pack_Decl := Unit_Declaration_Node (Spec_Id); @@ -719,6 +727,19 @@ package body Sem_Ch7 is Set_SPARK_Aux_Pragma_Inherited (Body_Id, True); end if; + -- Inherit the "ghostness" of the subprogram spec. Note that this + -- property is not directly inherited as the body may be subject to a + -- different Ghost assertion policy. + + if Is_Ghost_Entity (Spec_Id) or else Within_Ghost_Scope then + Set_Is_Ghost_Entity (Body_Id); + + -- The Ghost policy in effect at the point of declaration and at the + -- point of completion must match (SPARK RM 6.9(14)). + + Check_Ghost_Completion (Spec_Id, Body_Id); + end if; + Set_Categorization_From_Pragmas (N); Install_Visible_Declarations (Spec_Id); @@ -1754,6 +1775,13 @@ package body Sem_Ch7 is New_Private_Type (N, Id, N); Set_Depends_On_Private (Id); + -- A type declared within a Ghost scope is automatically Ghost + -- (SPARK RM 6.9(2)). + + if Within_Ghost_Scope then + Set_Is_Ghost_Entity (Id); + end if; + if Has_Aspects (N) then Analyze_Aspect_Specifications (N, Id); end if; @@ -2410,6 +2438,82 @@ package body Sem_Ch7 is end if; end New_Private_Type; + --------------------------------- + -- Requires_Completion_In_Body -- + --------------------------------- + + function Requires_Completion_In_Body + (Id : Entity_Id; + Pack_Id : Entity_Id) return Boolean is + begin + -- Always ignore child units. Child units get added to the entity list + -- of a parent unit, but are not original entities of the parent, and + -- so do not affect whether the parent needs a body. + + if Is_Child_Unit (Id) then + return False; + + -- Ignore formal packages and their renamings + + elsif Ekind (Id) = E_Package + and then Nkind (Original_Node (Unit_Declaration_Node (Id))) = + N_Formal_Package_Declaration + then + return False; + + -- A Ghost entity declared in a non-Ghost package does not force the + -- need for a body (SPARK RM 6.9(11)). + + elsif not Is_Ghost_Entity (Pack_Id) and then Is_Ghost_Entity (Id) then + return False; + + -- Otherwise test to see if entity requires a completion. Note that + -- subprogram entities whose declaration does not come from source are + -- ignored here on the basis that we assume the expander will provide an + -- implicit completion at some point. + + elsif (Is_Overloadable (Id) + and then Ekind (Id) /= E_Enumeration_Literal + and then Ekind (Id) /= E_Operator + and then not Is_Abstract_Subprogram (Id) + and then not Has_Completion (Id) + and then Comes_From_Source (Parent (Id))) + + or else + (Ekind (Id) = E_Package + and then Id /= Pack_Id + and then not Has_Completion (Id) + and then Unit_Requires_Body (Id)) + + or else + (Ekind (Id) = E_Incomplete_Type + and then No (Full_View (Id)) + and then not Is_Generic_Type (Id)) + + or else + (Ekind_In (Id, E_Task_Type, E_Protected_Type) + and then not Has_Completion (Id)) + + or else + (Ekind (Id) = E_Generic_Package + and then Id /= Pack_Id + and then not Has_Completion (Id) + and then Unit_Requires_Body (Id)) + + or else + (Is_Generic_Subprogram (Id) + and then not Has_Completion (Id)) + + then + return True; + + -- Otherwise the entity does not require completion in a package body + + else + return False; + end if; + end Requires_Completion_In_Body; + ---------------------------- -- Uninstall_Declarations -- ---------------------------- @@ -2859,7 +2963,7 @@ package body Sem_Ch7 is ------------------------ function Unit_Requires_Body - (P : Entity_Id; + (Pack_Id : Entity_Id; Ignore_Abstract_State : Boolean := False) return Boolean is E : Entity_Id; @@ -2869,30 +2973,30 @@ package body Sem_Ch7 is -- be imported, but perhaps in the future we will allow import of -- packages. - if Is_Imported (P) then + if Is_Imported (Pack_Id) then return False; -- Body required if library package with pragma Elaborate_Body - elsif Has_Pragma_Elaborate_Body (P) then + elsif Has_Pragma_Elaborate_Body (Pack_Id) then return True; -- Body required if subprogram - elsif Is_Subprogram_Or_Generic_Subprogram (P) then + elsif Is_Subprogram_Or_Generic_Subprogram (Pack_Id) then return True; -- Treat a block as requiring a body - elsif Ekind (P) = E_Block then + elsif Ekind (Pack_Id) = E_Block then return True; - elsif Ekind (P) = E_Package - and then Nkind (Parent (P)) = N_Package_Specification - and then Present (Generic_Parent (Parent (P))) + elsif Ekind (Pack_Id) = E_Package + and then Nkind (Parent (Pack_Id)) = N_Package_Specification + and then Present (Generic_Parent (Parent (Pack_Id))) then declare - G_P : constant Entity_Id := Generic_Parent (Parent (P)); + G_P : constant Entity_Id := Generic_Parent (Parent (Pack_Id)); begin if Has_Pragma_Elaborate_Body (G_P) then return True; @@ -2906,78 +3010,21 @@ package body Sem_Ch7 is -- provided). If Ignore_Abstract_State is True, we don't do this check -- (so we can use Unit_Requires_Body to check for some other reason). - elsif Ekind_In (P, E_Generic_Package, E_Package) + elsif Ekind_In (Pack_Id, E_Generic_Package, E_Package) and then not Ignore_Abstract_State - and then Present (Abstract_States (P)) - and then not Is_Null_State (Node (First_Elmt (Abstract_States (P)))) + and then Present (Abstract_States (Pack_Id)) + and then not Is_Null_State + (Node (First_Elmt (Abstract_States (Pack_Id)))) then return True; end if; -- Otherwise search entity chain for entity requiring completion - E := First_Entity (P); + E := First_Entity (Pack_Id); while Present (E) loop - - -- Always ignore child units. Child units get added to the entity - -- list of a parent unit, but are not original entities of the - -- parent, and so do not affect whether the parent needs a body. - - if Is_Child_Unit (E) then - null; - - -- Ignore formal packages and their renamings - - elsif Ekind (E) = E_Package - and then Nkind (Original_Node (Unit_Declaration_Node (E))) = - N_Formal_Package_Declaration - then - null; - - -- Otherwise test to see if entity requires a completion. - -- Note that subprogram entities whose declaration does not come - -- from source are ignored here on the basis that we assume the - -- expander will provide an implicit completion at some point. - - elsif (Is_Overloadable (E) - and then Ekind (E) /= E_Enumeration_Literal - and then Ekind (E) /= E_Operator - and then not Is_Abstract_Subprogram (E) - and then not Has_Completion (E) - and then Comes_From_Source (Parent (E))) - - or else - (Ekind (E) = E_Package - and then E /= P - and then not Has_Completion (E) - and then Unit_Requires_Body (E)) - - or else - (Ekind (E) = E_Incomplete_Type - and then No (Full_View (E)) - and then not Is_Generic_Type (E)) - - or else - (Ekind_In (E, E_Task_Type, E_Protected_Type) - and then not Has_Completion (E)) - - or else - (Ekind (E) = E_Generic_Package - and then E /= P - and then not Has_Completion (E) - and then Unit_Requires_Body (E)) - - or else - (Is_Generic_Subprogram (E) - and then not Has_Completion (E)) - - then + if Requires_Completion_In_Body (E, Pack_Id) then return True; - - -- Entity that does not require completion - - else - null; end if; Next_Entity (E); @@ -2990,40 +3037,40 @@ package body Sem_Ch7 is -- Unit_Requires_Body_Info -- ----------------------------- - procedure Unit_Requires_Body_Info (P : Entity_Id) is + procedure Unit_Requires_Body_Info (Pack_Id : Entity_Id) is E : Entity_Id; begin - -- Imported entity never requires body. Right now, only subprograms can - -- be imported, but perhaps in the future we will allow import of + -- An imported entity never requires body. Right now, only subprograms + -- can be imported, but perhaps in the future we will allow import of -- packages. - if Is_Imported (P) then + if Is_Imported (Pack_Id) then return; -- Body required if library package with pragma Elaborate_Body - elsif Has_Pragma_Elaborate_Body (P) then - Error_Msg_N ("info: & requires body (Elaborate_Body)?Y?", P); + elsif Has_Pragma_Elaborate_Body (Pack_Id) then + Error_Msg_N ("info: & requires body (Elaborate_Body)?Y?", Pack_Id); -- Body required if subprogram - elsif Is_Subprogram_Or_Generic_Subprogram (P) then - Error_Msg_N ("info: & requires body (subprogram case)?Y?", P); + elsif Is_Subprogram_Or_Generic_Subprogram (Pack_Id) then + Error_Msg_N ("info: & requires body (subprogram case)?Y?", Pack_Id); -- Body required if generic parent has Elaborate_Body - elsif Ekind (P) = E_Package - and then Nkind (Parent (P)) = N_Package_Specification - and then Present (Generic_Parent (Parent (P))) + elsif Ekind (Pack_Id) = E_Package + and then Nkind (Parent (Pack_Id)) = N_Package_Specification + and then Present (Generic_Parent (Parent (Pack_Id))) then declare - G_P : constant Entity_Id := Generic_Parent (Parent (P)); + G_P : constant Entity_Id := Generic_Parent (Parent (Pack_Id)); begin if Has_Pragma_Elaborate_Body (G_P) then Error_Msg_N ("info: & requires body (generic parent Elaborate_Body)?Y?", - P); + Pack_Id); end if; end; @@ -3034,79 +3081,24 @@ package body Sem_Ch7 is -- provided). If Ignore_Abstract_State is True, we don't do this check -- (so we can use Unit_Requires_Body to check for some other reason). - elsif Ekind_In (P, E_Generic_Package, E_Package) - and then Present (Abstract_States (P)) - and then not Is_Null_State (Node (First_Elmt (Abstract_States (P)))) + elsif Ekind_In (Pack_Id, E_Generic_Package, E_Package) + and then Present (Abstract_States (Pack_Id)) + and then not Is_Null_State + (Node (First_Elmt (Abstract_States (Pack_Id)))) then Error_Msg_N - ("info: & requires body (non-null abstract state aspect)?Y?", P); + ("info: & requires body (non-null abstract state aspect)?Y?", + Pack_Id); end if; -- Otherwise search entity chain for entity requiring completion - E := First_Entity (P); + E := First_Entity (Pack_Id); while Present (E) loop - - -- Always ignore child units. Child units get added to the entity - -- list of a parent unit, but are not original entities of the - -- parent, and so do not affect whether the parent needs a body. - - if Is_Child_Unit (E) then - null; - - -- Ignore formal packages and their renamings - - elsif Ekind (E) = E_Package - and then Nkind (Original_Node (Unit_Declaration_Node (E))) = - N_Formal_Package_Declaration - then - null; - - -- Otherwise test to see if entity requires a completion. - -- Note that subprogram entities whose declaration does not come - -- from source are ignored here on the basis that we assume the - -- expander will provide an implicit completion at some point. - - elsif (Is_Overloadable (E) - and then Ekind (E) /= E_Enumeration_Literal - and then Ekind (E) /= E_Operator - and then not Is_Abstract_Subprogram (E) - and then not Has_Completion (E) - and then Comes_From_Source (Parent (E))) - - or else - (Ekind (E) = E_Package - and then E /= P - and then not Has_Completion (E) - and then Unit_Requires_Body (E)) - - or else - (Ekind (E) = E_Incomplete_Type - and then No (Full_View (E)) - and then not Is_Generic_Type (E)) - - or else - (Ekind_In (E, E_Task_Type, E_Protected_Type) - and then not Has_Completion (E)) - - or else - (Ekind (E) = E_Generic_Package - and then E /= P - and then not Has_Completion (E) - and then Unit_Requires_Body (E)) - - or else - (Is_Generic_Subprogram (E) - and then not Has_Completion (E)) - then + if Requires_Completion_In_Body (E, Pack_Id) then Error_Msg_Node_2 := E; Error_Msg_NE - ("info: & requires body (& requires completion)?Y?", E, P); - - -- Entity that does not require completion - - else - null; + ("info: & requires body (& requires completion)?Y?", E, Pack_Id); end if; Next_Entity (E); diff --git a/gcc/ada/sem_ch7.ads b/gcc/ada/sem_ch7.ads index b74e4667b4c..a243ac5f3dc 100644 --- a/gcc/ada/sem_ch7.ads +++ b/gcc/ada/sem_ch7.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 1992-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2014, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -67,17 +67,17 @@ package Sem_Ch7 is -- child for public child packages. function Unit_Requires_Body - (P : Entity_Id; + (Pack_Id : Entity_Id; Ignore_Abstract_State : Boolean := False) return Boolean; - -- Check if a unit requires a body. A specification requires a body if it - -- contains declarations that require completion in a body. If the flag - -- Ignore_Abstract_State is set True, then the test for a non-null abstract - -- state (which normally requires a body) is not carried out. This allows - -- the use of this routine to tell if there is some other reason that a - -- body is required (as is required for analyzing Abstract_State). This - -- is not currently used, but may be useful in future if we implement a - -- compatibility mode which warns about possible incompatibilities if a - -- SPARK 2014 program is compiled with a SPARK-unaware compiler. + -- Determine whether package Pack_Id requires a body. A specification needs + -- a body if it contains declarations that require completion in the body. + -- A non-Ghost [generic] package does not require a body when it declares + -- Ghost entities exclusively. If flag Ignore_Abstract_State is True, then + -- the test for a non-null abstract state (which normally requires a body) + -- is not carried out. The flag is not currently used, but may be useful + -- in the future if we implement a compatibility mode which warns about + -- possible incompatibilities if a SPARK 2014 program is compiled with a + -- SPARK-unaware compiler. procedure May_Need_Implicit_Body (E : Entity_Id); -- If a package declaration contains tasks or RACWs and does not require diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index 798564c23c0..21d9e73d425 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -561,8 +561,8 @@ package body Sem_Ch8 is Set_Etype (Id, Standard_Exception_Type); Set_Is_Pure (Id, Is_Pure (Current_Scope)); - if not Is_Entity_Name (Nam) or else - Ekind (Entity (Nam)) /= E_Exception + if not Is_Entity_Name (Nam) + or else Ekind (Entity (Nam)) /= E_Exception then Error_Msg_N ("invalid exception name in renaming", Nam); else @@ -571,6 +571,13 @@ package body Sem_Ch8 is else Set_Renamed_Object (Id, Entity (Nam)); end if; + + -- An exception renaming is Ghost if the renamed entity is Ghost or + -- the construct appears within a Ghost scope. + + if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then + Set_Is_Ghost_Entity (Id); + end if; end if; -- Implementation-defined aspect specifications can appear in a renaming @@ -701,6 +708,13 @@ package body Sem_Ch8 is Set_Etype (New_P, Etype (Old_P)); Set_Has_Completion (New_P); + -- An generic renaming is Ghost if the renamed entity is Ghost or the + -- construct appears within a Ghost scope. + + if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then + Set_Is_Ghost_Entity (New_P); + end if; + if In_Open_Scopes (Old_P) then Error_Msg_N ("within its scope, generic denotes its instance", N); end if; @@ -849,7 +863,7 @@ package body Sem_Ch8 is if Nkind (Nam) = N_Selected_Component and then Analyzed (Nam) then T := Etype (Nam); - Dec := Build_Actual_Subtype_Of_Component (Etype (Nam), Nam); + Dec := Build_Actual_Subtype_Of_Component (Etype (Nam), Nam); if Present (Dec) then Insert_Action (N, Dec); @@ -1295,6 +1309,16 @@ package body Sem_Ch8 is Set_Is_True_Constant (Id, True); end if; + -- An object renaming is Ghost if the renamed entity is Ghost or the + -- construct appears within a Ghost scope. + + if (Is_Entity_Name (Nam) + and then Is_Ghost_Entity (Entity (Nam))) + or else Within_Ghost_Scope + then + Set_Is_Ghost_Entity (Id); + end if; + -- The entity of the renaming declaration needs to reflect whether the -- renamed object is volatile. Is_Volatile is set if the renamed object -- is volatile in the RM legality sense. @@ -1409,6 +1433,13 @@ package body Sem_Ch8 is Check_Library_Unit_Renaming (N, Old_P); Generate_Reference (Old_P, Name (N)); + -- A package renaming is Ghost if the renamed entity is Ghost or + -- the construct appears within a Ghost scope. + + if Is_Ghost_Entity (Old_P) or else Within_Ghost_Scope then + Set_Is_Ghost_Entity (New_P); + end if; + -- If the renaming is in the visible part of a package, then we set -- Renamed_In_Spec for the renamed package, to prevent giving -- warnings about no entities referenced. Such a warning would be @@ -2992,6 +3023,13 @@ package body Sem_Ch8 is Set_Is_Pure (New_S, Is_Pure (Entity (Nam))); Set_Is_Preelaborated (New_S, Is_Preelaborated (Entity (Nam))); + -- A subprogram renaming is Ghost if the renamed entity is Ghost or + -- the construct appears within a Ghost scope. + + if Is_Ghost_Entity (Entity (Nam)) or else Within_Ghost_Scope then + Set_Is_Ghost_Entity (New_S); + end if; + -- Ada 2005 (AI-423): Check the consistency of null exclusions -- between a subprogram and its correct renaming. diff --git a/gcc/ada/sem_mech.adb b/gcc/ada/sem_mech.adb index e37aefab020..2347bff46a0 100644 --- a/gcc/ada/sem_mech.adb +++ b/gcc/ada/sem_mech.adb @@ -149,7 +149,6 @@ package body Sem_Mech is when Convention_Ada | Convention_Intrinsic | Convention_Entry | - Convention_Ghost | Convention_Protected | Convention_Stubbed => diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 3f0b9b83345..e5c3d855c75 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -6514,11 +6514,7 @@ package body Sem_Prag is (C : out Convention_Id; Ent : out Entity_Id) is - Id : Node_Id; - E : Entity_Id; - E1 : Entity_Id; - Cname : Name_Id; - Comp_Unit : Unit_Number_Type; + Cname : Name_Id; procedure Diagnose_Multiple_Pragmas (S : Entity_Id); -- Called if we have more than one Export/Import/Convention pragma. @@ -6698,17 +6694,6 @@ package body Sem_Prag is procedure Set_Convention_From_Pragma (E : Entity_Id) is begin - -- Ghost convention is allowed only for functions - - if Ekind (E) /= E_Function and then C = Convention_Ghost then - Error_Msg_N - ("& may not have Ghost convention", E); - Error_Msg_N - ("\only functions are permitted to have Ghost convention", - E); - return; - end if; - -- Ada 2005 (AI-430): Check invalid attempt to change convention -- for an overridden dispatching operation. Technically this is -- an amendment and should only be done in Ada 2005 mode. However, @@ -6719,16 +6704,9 @@ package body Sem_Prag is and then Present (Overridden_Operation (E)) and then C /= Convention (Overridden_Operation (E)) then - -- An attempt to override a function with a ghost function - -- appears as a mismatch in conventions. - - if C = Convention_Ghost then - Error_Msg_N ("ghost function & cannot be overriding", E); - else - Error_Pragma_Arg - ("cannot change convention for overridden dispatching " - & "operation", Arg1); - end if; + Error_Pragma_Arg + ("cannot change convention for overridden dispatching " + & "operation", Arg1); end if; -- Special checks for Convention_Stdcall @@ -6858,6 +6836,13 @@ package body Sem_Prag is end if; end Set_Convention_From_Pragma; + -- Local variables + + Comp_Unit : Unit_Number_Type; + E : Entity_Id; + E1 : Entity_Id; + Id : Node_Id; + -- Start of processing for Process_Convention begin @@ -6919,11 +6904,10 @@ package body Sem_Prag is ("convention `Ada_Pass_By_Copy` not allowed for by-reference " & "type", Arg1); end if; - end if; -- Ada_Pass_By_Reference special checking - if C = Convention_Ada_Pass_By_Reference then + elsif C = Convention_Ada_Pass_By_Reference then if not Is_First_Subtype (E) then Error_Pragma_Arg ("convention `Ada_Pass_By_Reference` only allowed for types", @@ -6937,14 +6921,6 @@ package body Sem_Prag is end if; end if; - -- Ghost special checking - - if Is_Ghost_Subprogram (E) - and then Present (Overridden_Operation (E)) - then - Error_Msg_N ("ghost function & cannot be overriding", E); - end if; - -- Go to renamed subprogram if present, since convention applies to -- the actual renamed entity, not to the renaming entity. If the -- subprogram is inherited, go to parent subprogram. @@ -6974,9 +6950,8 @@ package body Sem_Prag is end if; end if; - -- Check that we are not applying this to a specless body - -- Relax this check if Relaxed_RM_Semantics to accomodate other Ada - -- compilers. + -- Check that we are not applying this to a specless body. Relax this + -- check if Relaxed_RM_Semantics to accomodate other Ada compilers. if Is_Subprogram (E) and then Nkind (Parent (Declaration_Node (E))) = N_Subprogram_Body @@ -9914,7 +9889,7 @@ package body Sem_Prag is -- SIMPLE_OPTION -- | NAME_VALUE_OPTION - -- SIMPLE_OPTION ::= identifier + -- SIMPLE_OPTION ::= Ghost -- NAME_VALUE_OPTION ::= -- Part_Of => ABSTRACT_STATE @@ -9945,20 +9920,22 @@ package body Sem_Prag is Non_Null_Seen : Boolean := False; Null_Seen : Boolean := False; - Pack_Id : Entity_Id; - -- Entity of related package when pragma Abstract_State appears - - procedure Analyze_Abstract_State (State : Node_Id); + procedure Analyze_Abstract_State + (State : Node_Id; + Pack_Id : Entity_Id); -- Verify the legality of a single state declaration. Create and -- decorate a state abstraction entity and introduce it into the - -- visibility chain. + -- visibility chain. Pack_Id denotes the entity or the related + -- package where pragma Abstract_State appears. ---------------------------- -- Analyze_Abstract_State -- ---------------------------- - procedure Analyze_Abstract_State (State : Node_Id) is - + procedure Analyze_Abstract_State + (State : Node_Id; + Pack_Id : Entity_Id) + is -- Flags used to verify the consistency of options AR_Seen : Boolean := False; @@ -10301,6 +10278,13 @@ package body Sem_Prag is Set_Refinement_Constituents (State_Id, New_Elmt_List); Set_Part_Of_Constituents (State_Id, New_Elmt_List); + -- An abstract state declared within a Ghost scope becomes + -- Ghost (SPARK RM 6.9(2)). + + if Within_Ghost_Scope then + Set_Is_Ghost_Entity (State_Id); + end if; + -- Establish a link between the state declaration and the -- abstract state entity. Note that a null state remains as -- N_Null and does not carry any linkages. @@ -10382,9 +10366,7 @@ package body Sem_Prag is Ancestor_Part (State)); end if; - -- Catch an attempt to introduce a simple option which is - -- currently not allowed. An exception to this is External - -- defined without any properties. + -- Options External and Ghost appear as expressions Opt := First (Expressions (State)); while Present (Opt) loop @@ -10392,6 +10374,11 @@ package body Sem_Prag is if Chars (Opt) = Name_External then Analyze_External_Option (Opt); + elsif Chars (Opt) = Name_Ghost then + if Present (State_Id) then + Set_Is_Ghost_Entity (State_Id); + end if; + -- Option Part_Of without an encapsulating state is -- illegal. (SPARK RM 7.1.4(9)). @@ -10514,6 +10501,7 @@ package body Sem_Prag is -- Local variables Context : constant Node_Id := Parent (Parent (N)); + Pack_Id : Entity_Id; State : Node_Id; -- Start of processing for Abstract_State @@ -10537,12 +10525,20 @@ package body Sem_Prag is State := Expression (Arg1); Pack_Id := Defining_Entity (Context); + -- Mark the associated package as Ghost if it is subject to aspect + -- or pragma Ghost as this affects the declaration of an abstract + -- state. + + if Is_Subject_To_Ghost (Unit_Declaration_Node (Pack_Id)) then + Set_Is_Ghost_Entity (Pack_Id); + end if; + -- Multiple non-null abstract states appear as an aggregate if Nkind (State) = N_Aggregate then State := First (Expressions (State)); while Present (State) loop - Analyze_Abstract_State (State); + Analyze_Abstract_State (State, Pack_Id); Next (State); end loop; @@ -10550,7 +10546,7 @@ package body Sem_Prag is -- include malformed state declarations. else - Analyze_Abstract_State (State); + Analyze_Abstract_State (State, Pack_Id); end if; -- Save the pragma for retrieval by other tools @@ -11073,6 +11069,7 @@ package body Sem_Prag is -- Contract_Cases | -- Debug | -- Default_Initial_Condition | + -- Ghost | -- Initial_Condition | -- Loop_Invariant | -- Loop_Variant | @@ -11916,7 +11913,8 @@ package body Sem_Prag is -- new form syntax. when Pragma_Check_Policy => Check_Policy : declare - Kind : Node_Id; + Ident : Node_Id; + Kind : Node_Id; begin GNAT_Pragma; @@ -11936,7 +11934,7 @@ package body Sem_Prag is -- identifier is Name. if Nkind (Arg1) /= N_Pragma_Argument_Association - or else Nam_In (Chars (Arg1), No_Name, Name_Name) + or else Nam_In (Chars (Arg1), No_Name, Name_Name) then -- Old syntax @@ -11950,8 +11948,8 @@ package body Sem_Prag is if Nam_In (Chars (Kind), Name_Name, Name_Policy) then Error_Msg_Name_2 := Chars (Kind); - Error_Pragma_Arg - ("pragma% does not allow% as check name", Arg1); + Error_Pragma_Arg + ("pragma% does not allow% as check name", Arg1); end if; -- Check policy @@ -11960,6 +11958,29 @@ package body Sem_Prag is 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 Within_Ghost_Scope 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 @@ -13910,7 +13931,7 @@ package body Sem_Prag is begin GNAT_Pragma; Check_No_Identifiers; - Check_At_Most_N_Arguments (1); + Check_At_Most_N_Arguments (1); Subp := Empty; Stmt := Prev (N); @@ -13955,7 +13976,8 @@ package body Sem_Prag is -- enclosing construct is the proper context. This check is done -- after the traversal above to allow for duplicate detection. - if Nkind (Context) = N_Subprogram_Body + if No (Subp) + and then Nkind (Context) = N_Subprogram_Body and then No (Corresponding_Spec (Context)) then Subp := Defining_Entity (Context); @@ -14187,6 +14209,212 @@ package body Sem_Prag is end if; end Finalize_Storage; + ----------- + -- Ghost -- + ----------- + + -- pragma Ghost [ (boolean_EXPRESSION) ]; + + when Pragma_Ghost => Ghost : declare + Context : constant Node_Id := Parent (N); + Expr : Node_Id; + Id : Entity_Id; + Orig_Stmt : Node_Id; + Prev_Id : Entity_Id; + Stmt : Node_Id; + + begin + GNAT_Pragma; + Check_No_Identifiers; + Check_At_Most_N_Arguments (1); + + Id := Empty; + Stmt := Prev (N); + while Present (Stmt) loop + + -- Skip prior pragmas, but check for duplicates + + if Nkind (Stmt) = N_Pragma then + if Pragma_Name (Stmt) = Pname then + Error_Msg_Name_1 := Pname; + Error_Msg_Sloc := Sloc (Stmt); + Error_Msg_N ("pragma % duplicates pragma declared#", N); + end if; + + -- Protected and task types cannot be subject to pragma Ghost + + elsif Nkind (Stmt) = N_Protected_Type_Declaration then + Error_Pragma ("pragma % cannot apply to a protected type"); + return; + + elsif Nkind (Stmt) = N_Task_Type_Declaration then + Error_Pragma ("pragma % cannot apply to a task type"); + return; + + -- Skip internally generated code + + elsif not Comes_From_Source (Stmt) then + Orig_Stmt := Original_Node (Stmt); + + -- When pragma Ghost applies to an untagged derivation, the + -- derivation is transformed into a [sub]type declaration. + + if Nkind_In (Stmt, N_Full_Type_Declaration, + N_Subtype_Declaration) + and then Comes_From_Source (Orig_Stmt) + and then Nkind (Orig_Stmt) = N_Full_Type_Declaration + and then Nkind (Type_Definition (Orig_Stmt)) = + N_Derived_Type_Definition + then + Id := Defining_Entity (Stmt); + exit; + + -- When pragma Ghost applies to an expression function, the + -- expression function is transformed into a subprogram. + + elsif Nkind (Stmt) = N_Subprogram_Declaration + and then Comes_From_Source (Orig_Stmt) + and then Nkind (Orig_Stmt) = N_Expression_Function + then + Id := Defining_Entity (Stmt); + exit; + end if; + + -- The pragma applies to a legal construct, stop the traversal + + elsif Nkind_In (Stmt, N_Abstract_Subprogram_Declaration, + N_Full_Type_Declaration, + N_Generic_Subprogram_Declaration, + N_Object_Declaration, + N_Private_Extension_Declaration, + N_Private_Type_Declaration, + N_Subprogram_Declaration, + N_Subtype_Declaration) + then + Id := Defining_Entity (Stmt); + exit; + + -- The pragma does not apply to a legal construct, issue an + -- error and stop the analysis. + + else + Error_Pragma + ("pragma % must apply to an object, package, subprogram " + & "or type"); + return; + end if; + + Stmt := Prev (Stmt); + end loop; + + if No (Id) then + + -- When pragma Ghost is associated with a [generic] package, it + -- appears in the visible declarations. + + if Nkind (Context) = N_Package_Specification + and then Present (Visible_Declarations (Context)) + and then List_Containing (N) = Visible_Declarations (Context) + then + Id := Defining_Entity (Context); + + -- Pragma Ghost applies to a stand alone subprogram body + + elsif Nkind (Context) = N_Subprogram_Body + and then No (Corresponding_Spec (Context)) + then + Id := Defining_Entity (Context); + end if; + end if; + + if No (Id) then + Error_Pragma + ("pragma % must apply to an object, package, subprogram or " + & "type"); + 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. + + if Is_Record_Type (Id) or else Ekind (Id) = E_Constant then + Prev_Id := Incomplete_Or_Partial_View (Id); + + if Present (Prev_Id) and then not Is_Ghost_Entity (Prev_Id) then + Error_Msg_Name_1 := Pname; + + -- 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)). + + if Ekind (Prev_Id) = E_Constant then + Error_Msg_Name_1 := Pname; + Error_Msg_NE (Fix_Error + ("pragma % must apply to declaration of deferred " + & "constant &"), N, Id); + return; + + -- Pragma Ghost may appear on the full view of an incomplete + -- type because the incomplete declaration lacks aspects and + -- cannot be subject to pragma Ghost. + + elsif Ekind (Prev_Id) = E_Incomplete_Type then + null; + + -- The full declaration of a type cannot be subject to + -- pragma Ghost unless the partial view is also Ghost + -- (SPARK RM 6.9(10)). + + else + Error_Msg_NE (Fix_Error + ("pragma % must apply to partial view of type &"), + N, Id); + return; + end if; + end if; + end if; + + -- Analyze the Boolean expression (if any) + + if Present (Arg1) then + Expr := Get_Pragma_Arg (Arg1); + + Analyze_And_Resolve (Expr, Standard_Boolean); + + if Is_OK_Static_Expression (Expr) then + + -- "Ghostness" cannot be turned off once enabled within a + -- region (SPARK RM 6.9(7)). + + if Is_False (Expr_Value (Expr)) + and then Within_Ghost_Scope + then + Error_Pragma + ("pragma % with value False cannot appear in enabled " + & "ghost region"); + return; + end if; + + -- Otherwie the expression is not static + + else + Error_Pragma_Arg + ("expression of pragma % must be static", Expr); + return; + end if; + end if; + + Set_Is_Ghost_Entity (Id); + end Ghost; + ------------ -- Global -- ------------ @@ -23087,6 +23315,12 @@ package body Sem_Prag is ------------------------- procedure Analyze_Constituent (Constit : Node_Id) is + procedure Check_Ghost_Constituent (Constit_Id : Entity_Id); + -- Verify that the constituent Constit_Id is a Ghost entity if the + -- abstract state being refined is also Ghost. If this is the case + -- verify that the Ghost policy in effect at the point of state + -- and constituent declaration is the same. + procedure Check_Matching_Constituent (Constit_Id : Entity_Id); -- Determine whether constituent Constit denoted by its entity -- Constit_Id appears in Hidden_States. Emit an error when the @@ -23169,6 +23403,7 @@ package body Sem_Prag is if Present (Encapsulating_State (Constit_Id)) then if Encapsulating_State (Constit_Id) = State_Id then + Check_Ghost_Constituent (Constit_Id); Remove (Part_Of_Constits, Constit_Id); Collect_Constituent; @@ -23197,6 +23432,8 @@ package body Sem_Prag is -- been encountered. if Node (State_Elmt) = Constit_Id then + Check_Ghost_Constituent (Constit_Id); + Remove_Elmt (Body_States, State_Elmt); Collect_Constituent; return; @@ -23217,6 +23454,59 @@ package body Sem_Prag is end if; end Check_Matching_Constituent; + ----------------------------- + -- Check_Ghost_Constituent -- + ----------------------------- + + procedure Check_Ghost_Constituent (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_Constituent; + -- Local variables Constit_Id : Entity_Id; @@ -25075,6 +25365,7 @@ package body Sem_Prag is Pragma_External_Name_Casing => 0, Pragma_Fast_Math => 0, Pragma_Finalize_Storage_Only => 0, + Pragma_Ghost => 0, Pragma_Global => -1, Pragma_Ident => -1, Pragma_Implementation_Defined => -1, @@ -25466,6 +25757,7 @@ package body Sem_Prag is Name_Contract_Cases | Name_Debug | Name_Default_Initial_Condition | + Name_Ghost | Name_Initial_Condition | Name_Invariant | Name_uInvariant | diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 97f6ea12c38..893e1e15ed8 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -109,6 +109,10 @@ package body Sem_Res is Pref : Node_Id); -- Check that the type of the prefix of a dereference is not incomplete + procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id); + -- Determine whether node Ghost_Ref appears within a Ghost-friendly context + -- where Ghost entity Ghost_Id can safely reside. + function Check_Infinite_Recursion (N : Node_Id) return Boolean; -- Given a call node, N, which is known to occur immediately within the -- subprogram being called, determines whether it is a detectable case of @@ -688,6 +692,193 @@ package body Sem_Res is end if; end Check_Fully_Declared_Prefix; + ------------------------- + -- Check_Ghost_Context -- + ------------------------- + + procedure Check_Ghost_Context (Ghost_Id : Entity_Id; Ghost_Ref : Node_Id) is + procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id); + -- Verify that the Ghost policy at the point of declaration of entity Id + -- matches the policy at the point of reference. If this is not the case + -- emit an error at Err_N. + + 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. + + ------------------------- + -- Is_OK_Ghost_Context -- + ------------------------- + + function Is_OK_Ghost_Context (Context : Node_Id) return Boolean is + function Is_Ghost_Declaration (Decl : Node_Id) return Boolean; + -- Determine whether node Decl is a Ghost declaration or appears + -- within a Ghost declaration. + + -------------------------- + -- Is_Ghost_Declaration -- + -------------------------- + + function Is_Ghost_Declaration (Decl : Node_Id) return Boolean is + Par : Node_Id; + Subp_Decl : Node_Id; + Subp_Id : Entity_Id; + + begin + -- Climb the parent chain looking for an object declaration + + Par := Decl; + while Present (Par) loop + case Nkind (Par) is + when N_Abstract_Subprogram_Declaration | + N_Exception_Declaration | + N_Exception_Renaming_Declaration | + N_Full_Type_Declaration | + N_Generic_Function_Renaming_Declaration | + N_Generic_Package_Declaration | + N_Generic_Package_Renaming_Declaration | + N_Generic_Procedure_Renaming_Declaration | + N_Generic_Subprogram_Declaration | + N_Number_Declaration | + N_Object_Declaration | + N_Object_Renaming_Declaration | + N_Package_Declaration | + N_Package_Renaming_Declaration | + N_Private_Extension_Declaration | + N_Private_Type_Declaration | + N_Subprogram_Declaration | + N_Subprogram_Renaming_Declaration | + N_Subtype_Declaration => + return Is_Subject_To_Ghost (Par); + + when others => + null; + end case; + + -- Special cases + + -- A reference to a Ghost entity may appear as the default + -- expression of a formal parameter of a subprogram body. This + -- context must be treated as suitable because the relation + -- between the spec and the body has not been established and + -- the body is not marked as Ghost yet. The real check was + -- performed on the spec. + + if Nkind (Par) = N_Parameter_Specification + and then Nkind (Parent (Parent (Par))) = N_Subprogram_Body + then + return True; + + -- References to Ghost entities may be relocated in internally + -- generated bodies. + + elsif Nkind (Par) = N_Subprogram_Body + and then not Comes_From_Source (Par) + then + Subp_Id := Corresponding_Spec (Par); + + -- The original context is an expression function that has + -- been split into a spec and a body. The context is OK as + -- long as the the initial declaration is Ghost. + + if Present (Subp_Id) then + Subp_Decl := + Original_Node (Unit_Declaration_Node (Subp_Id)); + + if Nkind (Subp_Decl) = N_Expression_Function then + return Is_Subject_To_Ghost (Subp_Decl); + end if; + end if; + + -- Otherwise this is either an internal body or an internal + -- completion. Both are OK because the real check was done + -- before expansion activities. + + return True; + end if; + + -- Prevent the search from going too far + + if Is_Body_Or_Package_Declaration (Par) then + return False; + end if; + + Par := Parent (Par); + end loop; + + return False; + end Is_Ghost_Declaration; + + -- Start of processing for Is_OK_Ghost_Context + + begin + -- The Ghost entity appears within an assertion expression + + if In_Assertion_Expr > 0 then + return True; + + -- The Ghost entity is part of a declaration or its completion + + elsif Is_Ghost_Declaration (Context) then + return True; + + -- The Ghost entity is referenced within a Ghost statement + + elsif Is_Ghost_Statement_Or_Pragma (Context) then + return True; + + else + return False; + end if; + end Is_OK_Ghost_Context; + + ------------------------ + -- Check_Ghost_Policy -- + ------------------------ + + procedure Check_Ghost_Policy (Id : Entity_Id; Err_N : Node_Id) is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + -- The Ghost policy in effect a the point of declaration and at the + -- 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); + + SPARK_Msg_N ("incompatible ghost policies in effect", Err_N); + SPARK_Msg_NE ("\& declared with ghost policy Check", Err_N, Id); + SPARK_Msg_NE ("\& used # with ghost policy Ignore", Err_N, Id); + + elsif Is_Ignored_Ghost_Entity (Id) and then Policy = Name_Check then + Error_Msg_Sloc := Sloc (Err_N); + + SPARK_Msg_N ("incompatible ghost policies in effect", Err_N); + SPARK_Msg_NE ("\& declared with ghost policy Ignore", Err_N, Id); + SPARK_Msg_NE ("\& used # with ghost policy Check", Err_N, Id); + end if; + end Check_Ghost_Policy; + + -- Start of processing for Check_Ghost_Context + + begin + -- Once it has been established that the reference to the Ghost entity + -- is within a suitable context, ensure that the policy at the point of + -- declaration and at the point of use match. + + if Is_OK_Ghost_Context (Ghost_Ref) then + Check_Ghost_Policy (Ghost_Id, Ghost_Ref); + + -- Otherwise the Ghost entity appears in a non-Ghost context and affects + -- its behavior or value. + + else + SPARK_Msg_N + ("ghost entity cannot appear in this context (SPARK RM 6.9(12))", + Ghost_Ref); + end if; + end Check_Ghost_Context; + ------------------------------ -- Check_Infinite_Recursion -- ------------------------------ @@ -5545,9 +5736,9 @@ package body Sem_Res is end if; if Is_Access_Subprogram_Type (Base_Type (Etype (Nam))) - and then not Is_Access_Subprogram_Type (Base_Type (Typ)) - and then Nkind (Subp) /= N_Explicit_Dereference - and then Present (Parameter_Associations (N)) + and then not Is_Access_Subprogram_Type (Base_Type (Typ)) + and then Nkind (Subp) /= N_Explicit_Dereference + and then Present (Parameter_Associations (N)) then -- The prefix is a parameterless function call that returns an access -- to subprogram. If parameters are present in the current call, add @@ -5808,6 +5999,12 @@ package body Sem_Res is Set_Is_Overloaded (Subp, False); Set_Is_Overloaded (N, False); + -- A Ghost entity must appear in a specific context + + if Is_Ghost_Entity (Nam) and then Comes_From_Source (N) then + Check_Ghost_Context (Nam, N); + end if; + -- If we are calling the current subprogram from immediately within its -- body, then that is the case where we can sometimes detect cases of -- infinite recursion statically. Do not try this in case restriction @@ -6855,38 +7052,48 @@ package body Sem_Res is Par := Parent (Par); end if; - -- An effectively volatile object subject to enabled properties - -- Async_Writers or Effective_Reads must appear in a specific context. -- The following checks are only relevant when SPARK_Mode is on as they -- are not standard Ada legality rules. - if SPARK_Mode = On - and then Is_Object (E) - and then Is_Effectively_Volatile (E) - and then Comes_From_Source (E) - and then - (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E)) - then - -- The effectively volatile objects appears in a "non-interfering - -- context" as defined in SPARK RM 7.1.3(13). + if SPARK_Mode = On then - if Is_OK_Volatile_Context (Par, N) then - null; + -- An effectively volatile object subject to enabled properties + -- Async_Writers or Effective_Reads must appear in a specific + -- context. + + if Is_Object (E) + and then Is_Effectively_Volatile (E) + and then + (Async_Writers_Enabled (E) or else Effective_Reads_Enabled (E)) + and then Comes_From_Source (N) + then + -- The effectively volatile objects appears in a "non-interfering + -- context" as defined in SPARK RM 7.1.3(13). - -- Assume that references to effectively volatile objects that appear - -- as actual parameters in a procedure call are always legal. A full - -- legality check is done when the actuals are resolved. + if Is_OK_Volatile_Context (Par, N) then + null; - elsif Nkind (Par) = N_Procedure_Call_Statement then - null; + -- Assume that references to effectively volatile objects that + -- appear as actual parameters in a procedure call are always + -- legal. A full legality check is done when the actuals are + -- resolved. - -- Otherwise the context causes a side effect with respect to the - -- effectively volatile object. + elsif Nkind (Par) = N_Procedure_Call_Statement then + null; - else - Error_Msg_N - ("volatile object cannot appear in this context " - & "(SPARK RM 7.1.3(13))", N); + -- Otherwise the context causes a side effect with respect to the + -- effectively volatile object. + + else + SPARK_Msg_N + ("volatile object cannot appear in this context " + & "(SPARK RM 7.1.3(13))", N); + end if; + + -- A Ghost entity must appear in a specific context + + elsif Is_Ghost_Entity (E) and then Comes_From_Source (N) then + Check_Ghost_Context (E, N); end if; end if; end Resolve_Entity_Name; diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 9fc89825ba7..793120f0bf6 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -2669,6 +2669,82 @@ package body Sem_Util is end if; end Check_Function_Writable_Actuals; + ---------------------------- + -- Check_Ghost_Completion -- + ---------------------------- + + procedure Check_Ghost_Completion + (Partial_View : Entity_Id; + Full_View : Entity_Id) + is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + -- The Ghost policy in effect at the point of declaration and at the + -- point of completion must match (SPARK RM 6.9(14)). + + if Is_Checked_Ghost_Entity (Partial_View) + and then Policy = Name_Ignore + then + Error_Msg_Sloc := Sloc (Full_View); + + SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View); + SPARK_Msg_N ("\& declared with ghost policy Check", Partial_View); + SPARK_Msg_N ("\& completed # with ghost policy Ignore", Partial_View); + + elsif Is_Ignored_Ghost_Entity (Partial_View) + and then Policy = Name_Check + then + Error_Msg_Sloc := Sloc (Full_View); + + SPARK_Msg_N ("incompatible ghost policies in effect", Partial_View); + SPARK_Msg_N ("\& declared with ghost policy Ignore", Partial_View); + SPARK_Msg_N ("\& completed # with ghost policy Check", Partial_View); + end if; + end Check_Ghost_Completion; + + ---------------------------- + -- 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 + SPARK_Msg_N ("type extension & cannot be ghost", Typ); + SPARK_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 + SPARK_Msg_N ("type extension & cannot be ghost", Typ); + SPARK_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_Implicit_Dereference -- -------------------------------- @@ -9306,15 +9382,15 @@ package body Sem_Util is end In_Visible_Part; -------------------------------- - -- Incomplete_Or_Private_View -- + -- Incomplete_Or_Partial_View -- -------------------------------- - function Incomplete_Or_Private_View (Typ : Entity_Id) return Entity_Id is + function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id is function Inspect_Decls (Decls : List_Id; Taft : Boolean := False) return Entity_Id; - -- Check whether a declarative region contains the incomplete or private - -- view of Typ. + -- Check whether a declarative region contains the incomplete or partial + -- view of Id. ------------------- -- Inspect_Decls -- @@ -9347,7 +9423,7 @@ package body Sem_Util is if Present (Match) and then Present (Full_View (Match)) - and then Full_View (Match) = Typ + and then Full_View (Match) = Id then return Match; end if; @@ -9365,14 +9441,14 @@ package body Sem_Util is -- Start of processing for Incomplete_Or_Partial_View begin - -- Incomplete type case + -- Deferred constant or incomplete type case - Prev := Current_Entity_In_Scope (Typ); + Prev := Current_Entity_In_Scope (Id); if Present (Prev) - and then Is_Incomplete_Type (Prev) + and then (Is_Incomplete_Type (Prev) or else Ekind (Prev) = E_Constant) and then Present (Full_View (Prev)) - and then Full_View (Prev) = Typ + and then Full_View (Prev) = Id then return Prev; end if; @@ -9380,7 +9456,7 @@ package body Sem_Util is -- Private or Taft amendment type case declare - Pkg : constant Entity_Id := Scope (Typ); + Pkg : constant Entity_Id := Scope (Id); Pkg_Decl : Node_Id := Pkg; begin @@ -9394,7 +9470,7 @@ package body Sem_Util is -- of this is when the two views have been exchanged - the full -- appears earlier than the private. - if Has_Private_Declaration (Typ) then + if Has_Private_Declaration (Id) then Prev := Inspect_Decls (Visible_Declarations (Pkg_Decl)); -- Exchanged view case, look in the private declarations @@ -9418,7 +9494,7 @@ package body Sem_Util is -- The type has no incomplete or private view return Empty; - end Incomplete_Or_Private_View; + end Incomplete_Or_Partial_View; ----------------------------------------- -- Inherit_Default_Init_Cond_Procedure -- @@ -11085,6 +11161,110 @@ package body Sem_Util is end if; end Is_Fully_Initialized_Variant; + --------------------- + -- Is_Ghost_Entity -- + --------------------- + + function Is_Ghost_Entity (Id : Entity_Id) return Boolean is + begin + return Is_Checked_Ghost_Entity (Id) or else Is_Ignored_Ghost_Entity (Id); + end Is_Ghost_Entity; + + ---------------------------------- + -- Is_Ghost_Statement_Or_Pragma -- + ---------------------------------- + + function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean is + function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean; + -- Determine whether an arbitrary node denotes a reference to a Ghost + -- entity. + + ------------------------------- + -- Is_Ghost_Entity_Reference -- + ------------------------------- + + function Is_Ghost_Entity_Reference (N : Node_Id) return Boolean is + Ref : Node_Id; + + begin + Ref := N; + + -- When the reference extracts a subcomponent, recover the related + -- object (SPARK RM 6.9(1)). + + while Nkind_In (Ref, N_Explicit_Dereference, + N_Indexed_Component, + N_Selected_Component, + N_Slice) + loop + Ref := Prefix (Ref); + end loop; + + return + Is_Entity_Name (Ref) + and then Present (Entity (Ref)) + and then Is_Ghost_Entity (Entity (Ref)); + end Is_Ghost_Entity_Reference; + + -- Local variables + + Arg : Node_Id; + Stmt : Node_Id; + + -- Start of processing for Is_Ghost_Statement_Or_Pragma + + begin + if Nkind (N) = N_Pragma then + + -- A pragma is Ghost when it appears within a Ghost package or + -- subprogram. + + if Within_Ghost_Scope then + return True; + end if; + + -- A pragma is Ghost when it mentions a Ghost entity + + Arg := First (Pragma_Argument_Associations (N)); + while Present (Arg) loop + if Is_Ghost_Entity_Reference (Get_Pragma_Arg (Arg)) then + return True; + end if; + + Next (Arg); + end loop; + end if; + + Stmt := N; + while Present (Stmt) loop + + -- A statement is Ghost when it appears within a Ghost package or + -- subprogram. + + if Is_Statement (Stmt) and then Within_Ghost_Scope then + return True; + + -- An assignment statement is Ghost when the target is a Ghost + -- variable. A procedure call is Ghost when the invoked procedure + -- is Ghost. + + elsif Nkind_In (Stmt, N_Assignment_Statement, + N_Procedure_Call_Statement) + then + return Is_Ghost_Entity_Reference (Name (Stmt)); + + -- Prevent the search from going too far + + elsif Is_Body_Or_Package_Declaration (Stmt) then + return False; + end if; + + Stmt := Parent (Stmt); + end loop; + + return False; + end Is_Ghost_Statement_Or_Pragma; + ---------------------------- -- Is_Inherited_Operation -- ---------------------------- @@ -12177,6 +12357,123 @@ package body Sem_Util is or else Nkind (N) = N_Procedure_Call_Statement; end Is_Statement; + ------------------------- + -- Is_Subject_To_Ghost -- + ------------------------- + + function Is_Subject_To_Ghost (N : Node_Id) return Boolean is + function Enables_Ghostness (Arg : Node_Id) return Boolean; + -- Determine whether aspect or pragma argument Arg enables "ghostness" + + ----------------------- + -- Enables_Ghostness -- + ----------------------- + + function Enables_Ghostness (Arg : Node_Id) return Boolean is + Expr : Node_Id; + + begin + Expr := Arg; + + if Nkind (Expr) = N_Pragma_Argument_Association then + Expr := Get_Pragma_Arg (Expr); + end if; + + -- Determine whether the expression of the aspect is static and + -- denotes True. + + if Present (Expr) then + Preanalyze_And_Resolve (Expr); + + return + Is_OK_Static_Expression (Expr) + and then Is_True (Expr_Value (Expr)); + + -- Otherwise Ghost defaults to True + + else + return True; + end if; + end Enables_Ghostness; + + -- Local variables + + Id : constant Entity_Id := Defining_Entity (N); + Asp : Node_Id; + Decl : Node_Id; + Prev_Id : Entity_Id; + + -- Start of processing for Is_Subject_To_Ghost + + begin + if Is_Ghost_Entity (Id) then + return True; + + -- The completion of a type or a constant is not fully analyzed when the + -- reference to the Ghost entity is resolved. Because the completion is + -- not marked as Ghost yet, inspect the partial view. + + elsif Is_Record_Type (Id) + or else Ekind (Id) = E_Constant + or else (Nkind (N) = N_Object_Declaration + and then Constant_Present (N)) + then + Prev_Id := Incomplete_Or_Partial_View (Id); + + if Present (Prev_Id) and then Is_Ghost_Entity (Prev_Id) then + return True; + end if; + end if; + + -- Examine the aspect specifications (if any) looking for aspect Ghost + + if Permits_Aspect_Specifications (N) then + Asp := First (Aspect_Specifications (N)); + while Present (Asp) loop + if Chars (Identifier (Asp)) = Name_Ghost then + return Enables_Ghostness (Expression (Asp)); + end if; + + Next (Asp); + end loop; + end if; + + Decl := Empty; + + -- When the context is a [generic] package declaration, pragma Ghost + -- resides in the visible declarations. + + if Nkind_In (N, N_Generic_Package_Declaration, + N_Package_Declaration) + then + Decl := First (Visible_Declarations (Specification (N))); + + -- Otherwise pragma Ghost appears in the declarations following N + + elsif Is_List_Member (N) then + Decl := Next (N); + end if; + + while Present (Decl) loop + if Nkind (Decl) = N_Pragma + and then Pragma_Name (Decl) = Name_Ghost + then + return + Enables_Ghostness (First (Pragma_Argument_Associations (Decl))); + + -- A source construct ends the region where pragma Ghost may appear, + -- stop the traversal. + + elsif Comes_From_Source (Decl) then + exit; + end if; + + Next (Decl); + end loop; + + return False; + end Is_Subject_To_Ghost; + -------------------------------------------------- -- Is_Subprogram_Stub_Without_Prior_Declaration -- -------------------------------------------------- @@ -15316,6 +15613,77 @@ package body Sem_Util is end if; end Original_Corresponding_Operation; + ---------------------- + -- Policy_In_Effect -- + ---------------------- + + function Policy_In_Effect (Policy : Name_Id) return Name_Id is + function Policy_In_List (List : Node_Id) return Name_Id; + -- Determine the the mode of a policy in a N_Pragma list + + -------------------- + -- Policy_In_List -- + -------------------- + + function Policy_In_List (List : Node_Id) return Name_Id is + Arg : Node_Id; + Expr : Node_Id; + Prag : Node_Id; + + begin + Prag := List; + while Present (Prag) loop + Arg := First (Pragma_Argument_Associations (Prag)); + Expr := Get_Pragma_Arg (Arg); + + -- The current Check_Policy pragma matches the requested policy, + -- return the second argument which denotes the policy identifier. + + if Chars (Expr) = Policy then + return Chars (Get_Pragma_Arg (Next (Arg))); + end if; + + Prag := Next_Pragma (Prag); + end loop; + + return No_Name; + end Policy_In_List; + + -- Local variables + + Kind : Name_Id; + + -- Start of processing for Policy_In_Effect + + begin + if not Is_Valid_Assertion_Kind (Policy) then + raise Program_Error; + end if; + + -- Inspect all policy pragmas that appear within scopes (if any) + + Kind := Policy_In_List (Check_Policy_List); + + -- Inspect all configuration policy pragmas (if any) + + if Kind = No_Name then + Kind := Policy_In_List (Check_Policy_List_Config); + end if; + + -- The context lacks policy pragmas, determine the mode based on whether + -- assertions are enabled. + + if Kind = No_Name then + if Assertions_Enabled then + Kind := Name_Check; + else + Kind := Name_Ignore; + end if; + end if; + + return Kind; + end Policy_In_Effect; + ---------------------------------- -- Predicate_Tests_On_Arguments -- ---------------------------------- @@ -16825,6 +17193,22 @@ package body Sem_Util is Set_Entity (N, Val); end Set_Entity_With_Checks; + ------------------------- + -- Set_Is_Ghost_Entity -- + ------------------------- + + procedure Set_Is_Ghost_Entity (Id : Entity_Id) is + Policy : constant Name_Id := Policy_In_Effect (Name_Ghost); + + begin + if Policy = Name_Check then + Set_Is_Checked_Ghost_Entity (Id); + + elsif Policy = Name_Ignore then + Set_Is_Ignored_Ghost_Entity (Id); + end if; + end Set_Is_Ghost_Entity; + ------------------------ -- Set_Name_Entity_Id -- ------------------------ @@ -17718,6 +18102,30 @@ package body Sem_Util is return List_1; end Visible_Ancestors; + ------------------------ + -- Within_Ghost_Scope -- + ------------------------ + + function Within_Ghost_Scope + (Id : Entity_Id := Current_Scope) return Boolean + is + S : Entity_Id; + + begin + -- Climb the scope stack looking for a Ghost scope + + S := Id; + while Present (S) and then S /= Standard_Standard loop + if Is_Ghost_Entity (S) then + return True; + end if; + + S := Scope (S); + end loop; + + return False; + end Within_Ghost_Scope; + ---------------------- -- Within_Init_Proc -- ---------------------- diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 5fdc5fb6c21..ff9c1697f94 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -285,6 +285,17 @@ package Sem_Util is -- the one containing C2, that is known to refer to the same object (RM -- 6.4.1(6.17/3)). + procedure Check_Ghost_Completion + (Partial_View : Entity_Id; + Full_View : Entity_Id); + -- Verify that the Ghost policy of a full view or a completion is the same + -- as the Ghost policy of the partial view. Emit an error if this is not + -- the case. + + 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_Implicit_Dereference (N : Node_Id; Typ : Entity_Id); -- AI05-139-2: Accessors and iterators for containers. This procedure -- checks whether T is a reference type, and if so it adds an interprettion @@ -1097,10 +1108,10 @@ package Sem_Util is -- package specification. The package must be on the scope stack, and the -- corresponding private part must not. - function Incomplete_Or_Private_View (Typ : Entity_Id) return Entity_Id; - -- Given the entity of a type, retrieve the incomplete or private view of - -- the same type. Note that Typ may not have a partial view to begin with, - -- in that case the function returns Empty. + function Incomplete_Or_Partial_View (Id : Entity_Id) return Entity_Id; + -- Given the entity of a constant or a type, retrieve the incomplete or + -- partial view of the same entity. Note that Id may not have a partial + -- view in which case the function returns Empty. procedure Inherit_Default_Init_Cond_Procedure (Typ : Entity_Id); -- Inherit the default initial condition procedure from the parent type of @@ -1268,6 +1279,18 @@ package Sem_Util is -- means that the result returned is not crucial, but should err on the -- side of thinking things are fully initialized if it does not know. + function Is_Ghost_Entity (Id : Entity_Id) return Boolean; + -- Determine whether entity Id is Ghost. To qualify as such, the entity + -- must be subject to Convention Ghost. + + function Is_Ghost_Statement_Or_Pragma (N : Node_Id) return Boolean; + -- Determine whether statement or pragma N is ghost. To qualify as such, N + -- must either + -- 1) Occur within a ghost subprogram or package + -- 2) Denote a call to a ghost procedure + -- 3) Denote an assignment statement whose target is a ghost variable + -- 4) Denote a pragma that mentions a ghost entity + function Is_Inherited_Operation (E : Entity_Id) return Boolean; -- E is a subprogram. Return True is E is an implicit operation inherited -- by a derived type declaration. @@ -1396,6 +1419,12 @@ package Sem_Util is -- the N_Statement_Other_Than_Procedure_Call subtype from Sinfo). -- Note that a label is *not* a statement, and will return False. + function Is_Subject_To_Ghost (N : Node_Id) return Boolean; + -- Determine whether declarative node N is subject to aspect or pragma + -- Ghost. Use this routine in cases where [source] pragma Ghost has not + -- been analyzed yet, but the context needs to establish the "ghostness" + -- of N. + function Is_Subprogram_Stub_Without_Prior_Declaration (N : Node_Id) return Boolean; -- Return True if N is a subprogram stub with no prior subprogram @@ -1680,6 +1709,10 @@ package Sem_Util is -- Name_uPre, Name_uPost, Name_uInvariant, or Name_uType_Invariant being -- returned to represent the corresponding aspects with x'Class names. + function Policy_In_Effect (Policy : Name_Id) return Name_Id; + -- Given a policy, return the policy identifier associated with it. If no + -- such policy is in effect, the value returned is No_Name. + function Predicate_Tests_On_Arguments (Subp : Entity_Id) return Boolean; -- Subp is the entity for a subprogram call. This function returns True if -- predicate tests are required for the arguments in this call (this is the @@ -1881,6 +1914,10 @@ package Sem_Util is -- If restriction No_Implementation_Identifiers is set, then it checks -- that the entity is not implementation defined. + procedure Set_Is_Ghost_Entity (Id : Entity_Id); + -- Set the relevant ghost attribute of entity Id depending on the current + -- Ghost assertion policy in effect. + procedure Set_Name_Entity_Id (Id : Name_Id; Val : Entity_Id); pragma Inline (Set_Name_Entity_Id); -- Sets the Entity_Id value associated with the given name, which is the @@ -2008,6 +2045,12 @@ package Sem_Util is -- generate the list of visible ancestors; otherwise their partial -- view is added to the resulting list. + function Within_Ghost_Scope + (Id : Entity_Id := Current_Scope) return Boolean; + -- Determine whether an arbitrary entity is either a scope or within a + -- scope subject to convention Ghost or one that inherits "ghostness" from + -- an enclosing construct. + function Within_Init_Proc return Boolean; -- Determines if Current_Scope is within an init proc diff --git a/gcc/ada/snames.adb-tmpl b/gcc/ada/snames.adb-tmpl index b0b5249851a..a198c428af5 100644 --- a/gcc/ada/snames.adb-tmpl +++ b/gcc/ada/snames.adb-tmpl @@ -155,7 +155,6 @@ package body Snames is when Name_COBOL => return Convention_COBOL; when Name_CPP => return Convention_CPP; when Name_Fortran => return Convention_Fortran; - when Name_Ghost => return Convention_Ghost; when Name_Intrinsic => return Convention_Intrinsic; when Name_Java => return Convention_Java; when Name_Stdcall => return Convention_Stdcall; @@ -193,7 +192,6 @@ package body Snames is when Convention_CPP => return Name_CPP; when Convention_Entry => return Name_Entry; when Convention_Fortran => return Name_Fortran; - when Convention_Ghost => return Name_Ghost; when Convention_Intrinsic => return Name_Intrinsic; when Convention_Java => return Name_Java; when Convention_Protected => return Name_Protected; diff --git a/gcc/ada/snames.ads-tmpl b/gcc/ada/snames.ads-tmpl index 42a9984a1c4..16ebf6ab142 100644 --- a/gcc/ada/snames.ads-tmpl +++ b/gcc/ada/snames.ads-tmpl @@ -497,6 +497,7 @@ package Snames is Name_Extensions_Visible : constant Name_Id := N + $; -- GNAT Name_External : constant Name_Id := N + $; -- GNAT Name_Finalize_Storage_Only : constant Name_Id := N + $; -- GNAT + Name_Ghost : constant Name_Id := N + $; -- GNAT Name_Global : constant Name_Id := N + $; -- GNAT Name_Ident : constant Name_Id := N + $; -- GNAT Name_Implementation_Defined : constant Name_Id := N + $; -- GNAT @@ -650,7 +651,6 @@ package Snames is Name_COBOL : constant Name_Id := N + $; Name_CPP : constant Name_Id := N + $; Name_Fortran : constant Name_Id := N + $; - Name_Ghost : constant Name_Id := N + $; Name_Intrinsic : constant Name_Id := N + $; Name_Java : constant Name_Id := N + $; Name_Stdcall : constant Name_Id := N + $; @@ -1651,12 +1651,11 @@ package Snames is type Convention_Id is ( -- The native-to-Ada (non-foreign) conventions come first. These include - -- the ones defined in the RM, plus Ghost and Stubbed. + -- the ones defined in the RM, plus Stubbed. Convention_Ada, Convention_Intrinsic, Convention_Entry, - Convention_Ghost, Convention_Protected, Convention_Stubbed, @@ -1832,6 +1831,7 @@ package Snames is Pragma_Extensions_Visible, Pragma_External, Pragma_Finalize_Storage_Only, + Pragma_Ghost, Pragma_Global, Pragma_Ident, Pragma_Implementation_Defined, -- 2.30.2