contracts.adb (Analyze_Object_Contract): Set and restore the SPARK_Mode for both constants and objects.

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* contracts.adb (Analyze_Object_Contract): Set and restore
	the SPARK_Mode for both constants and objects. Factor out the
	semantic checks concerning Ghost objects.
	* freeze.adb (Freeze_Array_Type): A Ghost array type cannot have a
	concurrent component type.
	(Freeze_Entity): A Ghost type cannot also be concurrent.
	(Freeze_Record_Type): A Ghost record type cannot have a concurrent
	component.
	* sem_prag.adb (Analyze_Abstract_State): A Ghost abstract
	state cannot also be synchronized.
	(Check_Ghost_Synchronous): New routine.
	* sem_util.adb (Yields_Synchronized_Object): Correct the case
	of record components to account for the case where the type has
	no component list.

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* expander.adb (Expand): Expand a single protected declaration.
	* exp_ch9.ads, exp_ch9.adb (Expand_N_Single_Protected_Declaration): New
	routine.

2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear
	in an object declaration as long as it denotes the name.

From-SVN: r229376

9 files changed, 184 insertions, 69 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 86893ba..7cafbd8 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,33 @@
 2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* contracts.adb (Analyze_Object_Contract): Set and restore
+	the SPARK_Mode for both constants and objects. Factor out the
+	semantic checks concerning Ghost objects.
+	* freeze.adb (Freeze_Array_Type): A Ghost array type cannot have a
+	concurrent component type.
+	(Freeze_Entity): A Ghost type cannot also be concurrent.
+	(Freeze_Record_Type): A Ghost record type cannot have a concurrent
+	component.
+	* sem_prag.adb (Analyze_Abstract_State): A Ghost abstract
+	state cannot also be synchronized.
+	(Check_Ghost_Synchronous): New routine.
+	* sem_util.adb (Yields_Synchronized_Object): Correct the case
+	of record components to account for the case where the type has
+	no component list.
+
+2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* expander.adb (Expand): Expand a single protected declaration.
+	* exp_ch9.ads, exp_ch9.adb (Expand_N_Single_Protected_Declaration): New
+	routine.
+
+2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_res.adb (Is_OK_Volatile_Context): A volatile object may appear
+	in an object declaration as long as it denotes the name.
+
+2015-10-26  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* sem_ch9.adb (Analyze_Single_Protected_Declaration): The anonymous
 	object no longer comes from source.
 	(Analyze_Single_Task_Declaration): The anonymous object no longer
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 30318dc..2ab91f9 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -648,10 +648,34 @@ package body Contracts is
          end if;
       end if;
 
+      --  The anonymous object created for a single concurrent type inherits
+      --  the SPARK_Mode from the type. Due to the timing of contract analysis,
+      --  delayed pragmas may be subject to the wrong SPARK_Mode, usually that
+      --  of the enclosing context. To remedy this, restore the original mode
+      --  of the related anonymous object.
+
+      if Is_Single_Concurrent_Object (Obj_Id)
+        and then Present (SPARK_Pragma (Obj_Id))
+      then
+         Restore_Mode := True;
+         Save_SPARK_Mode_And_Set (Obj_Id, Mode);
+      end if;
+
       --  Constant-related checks
 
       if Ekind (Obj_Id) = E_Constant then
 
+         --  Analyze indicator Part_Of
+
+         Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
+
+         --  Check whether the lack of indicator Part_Of agrees with the
+         --  placement of the constant with respect to the state space.
+
+         if No (Prag) then
+            Check_Missing_Part_Of (Obj_Id);
+         end if;
+
          --  A constant cannot be effectively volatile (SPARK RM 7.1.3(4)).
          --  This check is relevant only when SPARK_Mode is on, as it is not
          --  a standard Ada legality rule. Internally-generated constants that
@@ -666,32 +690,10 @@ package body Contracts is
             Error_Msg_N ("constant cannot be volatile", Obj_Id);
          end if;
 
-         Prag := Get_Pragma (Obj_Id, Pragma_Part_Of);
-
-         --  Check whether the lack of indicator Part_Of agrees with the
-         --  placement of the constant with respect to the state space.
-
-         if No (Prag) then
-            Check_Missing_Part_Of (Obj_Id);
-         end if;
-
       --  Variable-related checks
 
       else pragma Assert (Ekind (Obj_Id) = E_Variable);
 
-         --  The anonymous object created for a single concurrent type inherits
-         --  the SPARK_Mode from the type. Due to the timing of contract
-         --  analysis, delayed pragmas may be subject to the wrong SPARK_Mode,
-         --  usually that of the enclosing context. To remedy this, restore the
-         --  original SPARK_Mode of the related variable.
-
-         if Is_Single_Concurrent_Object (Obj_Id)
-           and then Present (SPARK_Pragma (Obj_Id))
-         then
-            Restore_Mode := True;
-            Save_SPARK_Mode_And_Set (Obj_Id, Mode);
-         end if;
-
          --  Analyze all external properties
 
          Prag := Get_Pragma (Obj_Id, Pragma_Async_Readers);
@@ -834,44 +836,42 @@ package body Contracts is
                   & "protected type %"), Obj_Id);
             end if;
          end if;
+      end if;
 
-         if Is_Ghost_Entity (Obj_Id) then
+      --  Common checks
 
-            --  A Ghost object cannot be effectively volatile (SPARK RM 6.9(8))
+      if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
 
-            if Is_Effectively_Volatile (Obj_Id) then
-               Error_Msg_N ("ghost variable & cannot be volatile", Obj_Id);
+         --  A Ghost object cannot be of a type that yields a synchronized
+         --  object (SPARK RM 6.9(19)).
 
-            --  A Ghost object cannot be imported or exported (SPARK RM 6.9(8))
+         if Yields_Synchronized_Object (Obj_Typ) then
+            Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id);
 
-            elsif Is_Imported (Obj_Id) then
-               Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
+         --  A Ghost object cannot be effectively volatile (SPARK RM 6.9(8) and
+         --  SPARK RM 6.9(19)).
 
-            elsif Is_Exported (Obj_Id) then
-               Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
-            end if;
-         end if;
+         elsif Is_Effectively_Volatile (Obj_Id) then
+            Error_Msg_N ("ghost object & cannot be volatile", Obj_Id);
 
-         --  Restore the SPARK_Mode of the enclosing context after all delayed
-         --  pragmas have been analyzed.
+         --  A Ghost object cannot be imported or exported (SPARK RM 6.9(8)).
+         --  One exception to this is the object that represents the dispatch
+         --  table of a Ghost tagged type, as the symbol needs to be exported.
 
-         if Restore_Mode then
-            Restore_SPARK_Mode (Mode);
-         end if;
-      end if;
-
-      --  A ghost object cannot be imported or exported (SPARK RM 6.9(8)). One
-      --  exception to this is the object that represents the dispatch table of
-      --  a Ghost tagged type, as the symbol needs to be exported.
-
-      if Comes_From_Source (Obj_Id) and then Is_Ghost_Entity (Obj_Id) then
-         if Is_Exported (Obj_Id) then
+         elsif Is_Exported (Obj_Id) then
             Error_Msg_N ("ghost object & cannot be exported", Obj_Id);
 
          elsif Is_Imported (Obj_Id) then
             Error_Msg_N ("ghost object & cannot be imported", Obj_Id);
          end if;
       end if;
+
+      --  Restore the SPARK_Mode of the enclosing context after all delayed
+      --  pragmas have been analyzed.
+
+      if Restore_Mode then
+         Restore_SPARK_Mode (Mode);
+      end if;
    end Analyze_Object_Contract;
 
    -----------------------------------
diff --git a/gcc/ada/exp_ch9.adb b/gcc/ada/exp_ch9.adb
index 00b3b60..4887c70 100644
--- a/gcc/ada/exp_ch9.adb
+++ b/gcc/ada/exp_ch9.adb
@@ -11388,14 +11388,28 @@ package body Exp_Ch9 is
       end loop;
    end Expand_N_Selective_Accept;
 
+   -------------------------------------------
+   -- Expand_N_Single_Protected_Declaration --
+   -------------------------------------------
+
+   --  A single protected declaration should never be present after semantic
+   --  analysis because it is transformed into a protected type declaration
+   --  and an accompanying anonymous object. This routine ensures that the
+   --  transformation takes place.
+
+   procedure Expand_N_Single_Protected_Declaration (N : Node_Id) is
+   begin
+      raise Program_Error;
+   end Expand_N_Single_Protected_Declaration;
+
    --------------------------------------
    -- Expand_N_Single_Task_Declaration --
    --------------------------------------
 
-   --  Single task declarations should never be present after semantic
-   --  analysis, since we expect them to be replaced by a declaration of an
-   --  anonymous task type, followed by a declaration of the task object. We
-   --  include this routine to make sure that is happening.
+   --  A single task declaration should never be present after semantic
+   --  analysis because it is transformed into a task type declaration and
+   --  an accompanying anonymous object. This routine ensures that the
+   --  transformation takes place.
 
    procedure Expand_N_Single_Task_Declaration (N : Node_Id) is
    begin
diff --git a/gcc/ada/exp_ch9.ads b/gcc/ada/exp_ch9.ads
index d9fa7d6..d49201b 100644
--- a/gcc/ada/exp_ch9.ads
+++ b/gcc/ada/exp_ch9.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2015, 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- --
@@ -266,12 +266,13 @@ package Exp_Ch9 is
    --  allows these two nodes to be found from the type, without benefit of
    --  further attributes, using Corresponding_Record.
 
-   procedure Expand_N_Requeue_Statement          (N : Node_Id);
-   procedure Expand_N_Selective_Accept           (N : Node_Id);
-   procedure Expand_N_Single_Task_Declaration    (N : Node_Id);
-   procedure Expand_N_Task_Body                  (N : Node_Id);
-   procedure Expand_N_Task_Type_Declaration      (N : Node_Id);
-   procedure Expand_N_Timed_Entry_Call           (N : Node_Id);
+   procedure Expand_N_Requeue_Statement            (N : Node_Id);
+   procedure Expand_N_Selective_Accept             (N : Node_Id);
+   procedure Expand_N_Single_Protected_Declaration (N : Node_Id);
+   procedure Expand_N_Single_Task_Declaration      (N : Node_Id);
+   procedure Expand_N_Task_Body                    (N : Node_Id);
+   procedure Expand_N_Task_Type_Declaration        (N : Node_Id);
+   procedure Expand_N_Timed_Entry_Call             (N : Node_Id);
 
    procedure Expand_Protected_Body_Declarations
      (N       : Node_Id;
diff --git a/gcc/ada/expander.adb b/gcc/ada/expander.adb
index 2d9b6d9..4aa20d6 100644
--- a/gcc/ada/expander.adb
+++ b/gcc/ada/expander.adb
@@ -432,6 +432,9 @@ package body Expander is
                when N_Selective_Accept =>
                   Expand_N_Selective_Accept (N);
 
+               when N_Single_Protected_Declaration =>
+                  Expand_N_Single_Protected_Declaration (N);
+
                when N_Single_Task_Declaration =>
                   Expand_N_Single_Task_Declaration (N);
 
@@ -471,7 +474,7 @@ package body Expander is
                when N_Variant_Part =>
                   Expand_N_Variant_Part (N);
 
-                  --  For all other node kinds, no expansion activity required
+               --  For all other node kinds, no expansion activity required
 
                when others =>
                   null;
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index e09fbd2..59a49ce 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -2806,6 +2806,15 @@ package body Freeze is
          then
             Set_Alignment (Arr, Alignment (Component_Type (Arr)));
          end if;
+
+         --  A Ghost type cannot have a component of protected or task type
+         --  (SPARK RM 6.9(19)).
+
+         if Is_Ghost_Entity (Arr) and then Is_Concurrent_Type (Ctyp) then
+            Error_Msg_N
+              ("ghost array type & cannot have concurrent component type",
+               Arr);
+         end if;
       end Freeze_Array_Type;
 
       -------------------------------
@@ -4341,6 +4350,25 @@ package body Freeze is
                   Next_Component (Comp);
                end loop;
             end if;
+
+            --  A Ghost type cannot have a component of protected or task type
+            --  (SPARK RM 6.9(19)).
+
+            if Is_Ghost_Entity (Rec) then
+               Comp := First_Component (Rec);
+               while Present (Comp) loop
+                  if Comes_From_Source (Comp)
+                    and then Is_Concurrent_Type (Etype (Comp))
+                  then
+                     Error_Msg_Name_1 := Chars (Rec);
+                     Error_Msg_N
+                       ("component & of ghost type % cannot be concurrent",
+                        Comp);
+                  end if;
+
+                  Next_Component (Comp);
+               end loop;
+            end if;
          end if;
 
          --  Make sure that if we have an iterator aspect, then we have
@@ -5091,12 +5119,19 @@ package body Freeze is
             end if;
          end;
 
-         --  A Ghost type cannot be effectively volatile (SPARK RM 6.9(8))
+         if Is_Ghost_Entity (E) then
 
-         if Is_Ghost_Entity (E)
-           and then Is_Effectively_Volatile (E)
-         then
-            Error_Msg_N ("ghost type & cannot be volatile", E);
+            --  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(8))
+
+            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
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index a8998cc..17544f0 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -10068,6 +10068,11 @@ package body Sem_Prag is
                --  Opt is not a duplicate property and sets the flag Status.
                --  (SPARK RM 7.1.4(2))
 
+               procedure Check_Ghost_Synchronous;
+               --  Ensure that the abstract state is not subject to both Ghost
+               --  and Synchronous simple options. Emit an error if this is the
+               --  case.
+
                procedure Create_Abstract_State
                  (Nam     : Name_Id;
                   Decl    : Node_Id;
@@ -10320,6 +10325,20 @@ package body Sem_Prag is
                   Status := True;
                end Check_Duplicate_Property;
 
+               -----------------------------
+               -- Check_Ghost_Synchronous --
+               -----------------------------
+
+               procedure Check_Ghost_Synchronous is
+               begin
+                  --  A synchronized abstract state cannot be Ghost and vice
+                  --  versa (SPARK RM 6.9(19)).
+
+                  if Ghost_Seen and Synchronous_Seen then
+                     SPARK_Msg_N ("synchronized state cannot be ghost", State);
+                  end if;
+               end Check_Ghost_Synchronous;
+
                ---------------------------
                -- Create_Abstract_State --
                ---------------------------
@@ -10464,6 +10483,7 @@ package body Sem_Prag is
 
                         elsif Chars (Opt) = Name_Ghost then
                            Check_Duplicate_Option (Opt, Ghost_Seen);
+                           Check_Ghost_Synchronous;
 
                            if Present (State_Id) then
                               Set_Is_Ghost_Entity (State_Id);
@@ -10473,6 +10493,7 @@ package body Sem_Prag is
 
                         elsif Chars (Opt) = Name_Synchronous then
                            Check_Duplicate_Option (Opt, Synchronous_Seen);
+                           Check_Ghost_Synchronous;
 
                         --  Option Part_Of without an encapsulating state is
                         --  illegal (SPARK RM 7.1.4(9)).
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index d2963f7..d3312e2 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -6993,6 +6993,13 @@ package body Sem_Res is
                return True;
             end if;
 
+         --  The volatile object acts as the name of a renaming declaration
+
+         elsif Nkind (Context) = N_Object_Renaming_Declaration
+           and then Name (Context) = Obj_Ref
+         then
+            return True;
+
          --  The volatile object appears as an actual parameter in a call to an
          --  instance of Unchecked_Conversion whose result is renamed.
 
diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb
index 8e33f4c..d8567c5 100644
--- a/gcc/ada/sem_util.adb
+++ b/gcc/ada/sem_util.adb
@@ -20121,7 +20121,8 @@ package body Sem_Util is
    --------------------------------
 
    function Yields_Synchronized_Object (Typ : Entity_Id) return Boolean is
-      Id : Entity_Id;
+      Has_Sync_Comp : Boolean := False;
+      Id            : Entity_Id;
 
    begin
       --  An array type yields a synchronized object if its component type
@@ -20154,10 +20155,15 @@ package body Sem_Util is
          Id := First_Entity (Typ);
          while Present (Id) loop
             if Comes_From_Source (Id) then
-               if Ekind (Id) = E_Component
-                 and then not Yields_Synchronized_Object (Etype (Id))
-               then
-                  return False;
+               if Ekind (Id) = E_Component then
+                  if Yields_Synchronized_Object (Etype (Id)) then
+                     Has_Sync_Comp := True;
+
+                  --  The component does not yield a synchronized object
+
+                  else
+                     return False;
+                  end if;
 
                elsif Ekind (Id) = E_Discriminant
                  and then Present (Expression (Parent (Id)))
@@ -20181,7 +20187,7 @@ package body Sem_Util is
          --  If we get here, then all discriminants lack default values and all
          --  components are of a type that yields a synchronized object.
 
-         return True;
+         return Has_Sync_Comp;
 
       --  A synchronized interface type yields a synchronized object by default