This patch ensures that single concurrent type declarations are marked as Ghost
when they appear within a Ghost region. In addition, the patch verifies that no
concurrent type is declared within a Ghost region and issues an error.
------------
-- Source --
------------
-- types.ads
package Types with Ghost is
protected Prot_Obj is -- Error
end Prot_Obj;
protected type Prot_Typ is -- Error
end Prot_Typ;
task Task_Obj; -- Error
task type Task_Typ; -- Error
end Types;
----------------------------
-- Compilation and output --
----------------------------
$ gcc -c types.ads
types.ads:2:14: ghost type "Prot_Obj" cannot be concurrent
types.ads:5:19: ghost type "Prot_Typ" cannot be concurrent
types.ads:8:09: ghost type "Task_Obj" cannot be concurrent
types.ads:10:14: ghost type "Task_Typ" cannot be concurrent
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-01-11 Hristian Kirtchev <kirtc...@adacore.com>
gcc/ada/
* freeze.adb (Freeze_Entity): Ensure that a Ghost type is not
concurrent, nor effectively volatile.
* ghost.adb (Check_Ghost_Type): New routine.
* ghost.ads (Check_Ghost_Type): New routine.
* sem_util.adb (Is_Declaration): Reimplemented. The routine can now
consider specific subsets of declarations.
(Is_Declaration_Other_Than_Renaming): Removed. Its functionality is
replicated by Is_Declaration.
* sem_util.ads (Is_Declaration): New parameter profile. Update the
comment on usage.
(Is_Declaration_Other_Than_Renaming): Removed.--- gcc/ada/freeze.adb
+++ gcc/ada/freeze.adb
@@ -5517,6 +5517,11 @@ package body Freeze is
-- Case of a type or subtype being frozen
else
+ -- Verify several SPARK legality rules related to Ghost types now
+ -- that the type is frozen.
+
+ Check_Ghost_Type (E);
+
-- We used to check here that a full type must have preelaborable
-- initialization if it completes a private type specified with
-- pragma Preelaborable_Initialization, but that missed cases where
@@ -5567,21 +5572,6 @@ package body Freeze is
end if;
end;
- if Is_Ghost_Entity (E) then
-
- -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify
- -- this legality rule first to five a finer-grained diagnostic.
-
- if Is_Concurrent_Type (E) then
- Error_Msg_N ("ghost type & cannot be concurrent", E);
-
- -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
-
- elsif Is_Effectively_Volatile (E) then
- Error_Msg_N ("ghost type & cannot be volatile", E);
- end if;
- end if;
-
-- Deal with special cases of freezing for subtype
if E /= Base_Type (E) then--- gcc/ada/ghost.adb
+++ gcc/ada/ghost.adb
@@ -806,6 +806,42 @@ package body Ghost is
end if;
end Check_Ghost_Refinement;
+ ----------------------
+ -- Check_Ghost_Type --
+ ----------------------
+
+ procedure Check_Ghost_Type (Typ : Entity_Id) is
+ Conc_Typ : Entity_Id;
+ Full_Typ : Entity_Id;
+
+ begin
+ if Is_Ghost_Entity (Typ) then
+ Conc_Typ := Empty;
+ Full_Typ := Typ;
+
+ if Is_Single_Concurrent_Type (Typ) then
+ Conc_Typ := Anonymous_Object (Typ);
+ Full_Typ := Conc_Typ;
+
+ elsif Is_Concurrent_Type (Typ) then
+ Conc_Typ := Typ;
+ end if;
+
+ -- A Ghost type cannot be concurrent (SPARK RM 6.9(19)). Verify this
+ -- legality rule first to give a finer-grained diagnostic.
+
+ if Present (Conc_Typ) then
+ Error_Msg_N ("ghost type & cannot be concurrent", Conc_Typ);
+ end if;
+
+ -- A Ghost type cannot be effectively volatile (SPARK RM 6.9(7))
+
+ if Is_Effectively_Volatile (Full_Typ) then
+ Error_Msg_N ("ghost type & cannot be volatile", Full_Typ);
+ end if;
+ end if;
+ end Check_Ghost_Type;
+
------------------
-- Ghost_Entity --
--------------------- gcc/ada/ghost.ads
+++ gcc/ada/ghost.ads
@@ -68,6 +68,10 @@ package Ghost is
-- Verify that the Ghost policy of constituent Constit_Id is compatible
-- with the Ghost policy of abstract state State_I.
+ procedure Check_Ghost_Type (Typ : Entity_Id);
+ -- Verify that Ghost type Typ is neither concurrent, nor effectively
+ -- volatile.
+
function Implements_Ghost_Interface (Typ : Entity_Id) return Boolean;
-- Determine whether type Typ implements at least one Ghost interface
--- gcc/ada/sem_util.adb
+++ gcc/ada/sem_util.adb
@@ -13368,40 +13368,113 @@ package body Sem_Util is
-- Is_Declaration --
--------------------
- function Is_Declaration (N : Node_Id) return Boolean is
+ function Is_Declaration
+ (N : Node_Id;
+ Body_OK : Boolean := True;
+ Concurrent_OK : Boolean := True;
+ Formal_OK : Boolean := True;
+ Generic_OK : Boolean := True;
+ Instantiation_OK : Boolean := True;
+ Renaming_OK : Boolean := True;
+ Stub_OK : Boolean := True;
+ Subprogram_OK : Boolean := True;
+ Type_OK : Boolean := True) return Boolean
+ is
begin
- return
- Is_Declaration_Other_Than_Renaming (N)
- or else Is_Renaming_Declaration (N);
- end Is_Declaration;
+ case Nkind (N) is
- ----------------------------------------
- -- Is_Declaration_Other_Than_Renaming --
- ----------------------------------------
+ -- Body declarations
+
+ when N_Proper_Body =>
+ return Body_OK;
+
+ -- Concurrent type declarations
+
+ when N_Protected_Type_Declaration
+ | N_Single_Protected_Declaration
+ | N_Single_Task_Declaration
+ | N_Task_Type_Declaration
+ =>
+ return Concurrent_OK or Type_OK;
+
+ -- Formal declarations
+
+ when N_Formal_Abstract_Subprogram_Declaration
+ | N_Formal_Concrete_Subprogram_Declaration
+ | N_Formal_Object_Declaration
+ | N_Formal_Package_Declaration
+ | N_Formal_Type_Declaration
+ =>
+ return Formal_OK;
+
+ -- Generic declarations
+
+ when N_Generic_Package_Declaration
+ | N_Generic_Subprogram_Declaration
+ =>
+ return Generic_OK;
+
+ -- Generic instantiations
+
+ when N_Function_Instantiation
+ | N_Package_Instantiation
+ | N_Procedure_Instantiation
+ =>
+ return Instantiation_OK;
+
+ -- Generic renaming declarations
+
+ when N_Generic_Renaming_Declaration =>
+ return Generic_OK or Renaming_OK;
+
+ -- Renaming declarations
+
+ when N_Exception_Renaming_Declaration
+ | N_Object_Renaming_Declaration
+ | N_Package_Renaming_Declaration
+ | N_Subprogram_Renaming_Declaration
+ =>
+ return Renaming_OK;
+
+ -- Stub declarations
+
+ when N_Body_Stub =>
+ return Stub_OK;
+
+ -- Subprogram declarations
- function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean is
- begin
- case Nkind (N) is
when N_Abstract_Subprogram_Declaration
- | N_Exception_Declaration
+ | N_Entry_Declaration
| N_Expression_Function
- | N_Full_Type_Declaration
- | N_Generic_Package_Declaration
- | N_Generic_Subprogram_Declaration
- | N_Number_Declaration
- | N_Object_Declaration
- | N_Package_Declaration
+ | N_Subprogram_Declaration
+ =>
+ return Subprogram_OK;
+
+ -- Type declarations
+
+ when N_Full_Type_Declaration
+ | N_Incomplete_Type_Declaration
| N_Private_Extension_Declaration
| N_Private_Type_Declaration
- | N_Subprogram_Declaration
| N_Subtype_Declaration
=>
+ return Type_OK;
+
+ -- Miscellaneous
+
+ when N_Component_Declaration
+ | N_Exception_Declaration
+ | N_Implicit_Label_Declaration
+ | N_Number_Declaration
+ | N_Object_Declaration
+ | N_Package_Declaration
+ =>
return True;
when others =>
return False;
end case;
- end Is_Declaration_Other_Than_Renaming;
+ end Is_Declaration;
--------------------------------
-- Is_Declared_Within_Variant ----- gcc/ada/sem_util.ads
+++ gcc/ada/sem_util.ads
@@ -1561,11 +1561,39 @@ package Sem_Util is
-- declarations. In Ada 2012 it also covers type and subtype declarations
-- with aspects: Invariant, Predicate, and Default_Initial_Condition.
- function Is_Declaration (N : Node_Id) return Boolean;
- -- Determine whether arbitrary node N denotes a declaration
-
- function Is_Declaration_Other_Than_Renaming (N : Node_Id) return Boolean;
- -- Determine whether arbitrary node N denotes a non-renaming declaration
+ function Is_Declaration
+ (N : Node_Id;
+ Body_OK : Boolean := True;
+ Concurrent_OK : Boolean := True;
+ Formal_OK : Boolean := True;
+ Generic_OK : Boolean := True;
+ Instantiation_OK : Boolean := True;
+ Renaming_OK : Boolean := True;
+ Stub_OK : Boolean := True;
+ Subprogram_OK : Boolean := True;
+ Type_OK : Boolean := True) return Boolean;
+ -- Determine whether arbitrary node N denotes a declaration depending
+ -- on the allowed subsets of declarations. Set the following flags to
+ -- consider specific subsets of declarations:
+ --
+ -- * Body_OK - body declarations
+ --
+ -- * Concurrent_OK - concurrent type declarations
+ --
+ -- * Formal_OK - formal declarations
+ --
+ -- * Generic_OK - generic declarations, including generic renamings
+ --
+ -- * Instantiation_OK - generic instantiations
+ --
+ -- * Renaming_OK - renaming declarations, including generic renamings
+ --
+ -- * Stub_OK - stub declarations
+ --
+ -- * Subprogram_OK - entry, expression function, and subprogram
+ -- declarations.
+ --
+ -- * Type_OK - type declarations, including concurrent types
function Is_Declared_Within_Variant (Comp : Entity_Id) return Boolean;
-- Returns True iff component Comp is declared within a variant part
