[Ada] Prohibit concurrent types in Ghost regions

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

2018-01-11  Hristian Kirtchev  <kirtchev@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.

From-SVN: r256521

6 files changed, 185 insertions, 40 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index cd66210..1eabde4 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,19 @@
 2018-01-11  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* 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.
+
+2018-01-11  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* sem_ch5.adb (Analyze_Assignment): Assignments to variables that act
 	as Part_Of consituents of single protected types are illegal when they
 	take place inside a protected function.
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index ba49b39..1e6e257 100644
--- a/gcc/ada/freeze.adb
+++ b/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
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 6dad9c2..5997724 100644
--- a/gcc/ada/ghost.adb
+++ b/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 --
    ------------------
diff --git a/gcc/ada/ghost.ads b/gcc/ada/ghost.ads
index 10fe447..8e23bcf 100644
--- a/gcc/ada/ghost.ads
+++ b/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
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index c72164b..5fa02dd 100644
--- a/gcc/ada/sem_util.adb
+++ b/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 --
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index a4ed966..3de3944 100644
--- a/gcc/ada/sem_util.ads
+++ b/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