[multiple changes]

2014-11-20  Robert Dewar  <dewar@adacore.com>

	* sem_prag.adb (Analyze_Pragma, case Elaborate): Forbid pragma
	Elaborate in SPARK mode.

2014-11-20  Bob Duff  <duff@adacore.com>

	* s-taskin.adb, s-tassta.adb (Initialize_ATCB): If Domain
	is null, then initialize T.Common.Domain to that of the
	activating task (not the parent task!), as required by RM-D.16.1.
	T.Common.Domain should never be null; so Assert. Remove similar
	code from Create_Task in s-tassta.adb.
	* s-mudido-affinity.adb: Remove checks for Domain = null,
	because it can't be null.
	* s-taskin.ads, s-taspri-dummy.ads, s-taspri-mingw.ads,
	s-taspri-posix.ads, s-taspri-posix-noaltstack.ads,
	s-taspri-solaris.ads, s-taspri-vxworks.ads: Mark limited types as
	explicitly limited for clarity.

2014-11-20  Ed Schonberg  <schonberg@adacore.com>

	* exp_aggr.adb (Init_Hidden_Discriminants): Code clean up.

From-SVN: r217863

gcc/ada/ChangeLog

@@ -1,3 +1,26 @@
+2014-11-20  Robert Dewar  <dewar@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma, case Elaborate): Forbid pragma
+	Elaborate in SPARK mode.
+
+2014-11-20  Bob Duff  <duff@adacore.com>
+
+	* s-taskin.adb, s-tassta.adb (Initialize_ATCB): If Domain
+	is null, then initialize T.Common.Domain to that of the
+	activating task (not the parent task!), as required by RM-D.16.1.
+	T.Common.Domain should never be null; so Assert. Remove similar
+	code from Create_Task in s-tassta.adb.
+	* s-mudido-affinity.adb: Remove checks for Domain = null,
+	because it can't be null.
+	* s-taskin.ads, s-taspri-dummy.ads, s-taspri-mingw.ads,
+	s-taspri-posix.ads, s-taspri-posix-noaltstack.ads,
+	s-taspri-solaris.ads, s-taspri-vxworks.ads: Mark limited types as
+	explicitly limited for clarity.
+
+2014-11-20  Ed Schonberg  <schonberg@adacore.com>
+
+	* exp_aggr.adb (Init_Hidden_Discriminants): Code clean up.
+
 2014-11-20  Robert Dewar  <dewar@adacore.com>
 
 	* errout.adb (Error_Msg): Don't suppress continuation msgs for

gcc/ada/exp_aggr.adb

@@ -2108,21 +2108,27 @@ package body Exp_Aggr is
       -------------------------------
 
       procedure Init_Hidden_Discriminants (Typ : Entity_Id; List : List_Id) is
-         Btype       : Entity_Id;
+         Btype        : Entity_Id;
-         Parent_Type : Entity_Id;
+         Parent_Type  : Entity_Id;
-         Disc        : Entity_Id;
+         Disc         : Entity_Id;
-         Discr_Val   : Elmt_Id;
+         Discr_Val    : Elmt_Id;
+         In_Aggr_Type : Boolean;
 
       begin
          --  The constraints on the hidden discriminants, if present, are kept
          --  in the Stored_Constraint list of the type itself, or in that of
-         --  the base type.
+         --  the base type. If not in the constraints of the aggregate itself,
+         --  we examine ancestors to find discriminants that are not renamed
+         --  by other discriminants but constrained explicitly.
+
+         In_Aggr_Type := True;
 
          Btype := Base_Type (Typ);
          while Is_Derived_Type (Btype)
            and then (Present (Stored_Constraint (Btype))
                        or else
-                     Present (Stored_Constraint (Typ)))
+                     (In_Aggr_Type
+                         and then Present (Stored_Constraint (Typ))))
          loop
             Parent_Type := Etype (Btype);
 
@@ -2149,7 +2155,7 @@ package body Exp_Aggr is
                Discr_Val := First_Elmt (Stored_Constraint (Typ));
             end if;
 
-            while Present (Discr_Val) loop
+            while Present (Discr_Val) and Present (Disc) loop
 
                --  Only those discriminants of the parent that are not
                --  renamed by discriminants of the derived type need to
@@ -2176,6 +2182,7 @@ package body Exp_Aggr is
                Next_Elmt (Discr_Val);
             end loop;
 
+            In_Aggr_Type := False;
             Btype := Base_Type (Parent_Type);
          end loop;
       end Init_Hidden_Discriminants;

gcc/ada/s-mudido-affinity.adb

@@ -85,8 +85,7 @@ package body System.Multiprocessors.Dispatching_Domains is
       --  System_Dispatching_Domain, or if CPU is not one of the processors of
       --  Domain (and is not Not_A_Specific_CPU).
 
-      if Target.Common.Domain /= null and then
+      if Dispatching_Domain (Target.Common.Domain) /= System_Dispatching_Domain
-        Dispatching_Domain (Target.Common.Domain) /= System_Dispatching_Domain
       then
          raise Dispatching_Domain_Error with
            "task already in user-defined dispatching domain";
@@ -201,9 +200,7 @@ package body System.Multiprocessors.Dispatching_Domains is
       T := ST.All_Tasks_List;
 
       while T /= null loop
-         if T.Common.Domain = null or else
+         if T.Common.Domain = ST.System_Domain then
-           T.Common.Domain = ST.System_Domain
-         then
             Set_Task_Affinity (T);
          end if;
 
@@ -275,7 +272,11 @@ package body System.Multiprocessors.Dispatching_Domains is
             Ada.Task_Identification.Current_Task) return Dispatching_Domain
    is
    begin
-      return Dispatching_Domain (Convert_Ids (T).Common.Domain);
+      return Result : constant Dispatching_Domain :=
+        Dispatching_Domain (Convert_Ids (T).Common.Domain)
+      do
+         pragma Assert (Result /= null);
+      end return;
    end Get_Dispatching_Domain;
 
    -------------------

gcc/ada/s-taskin.adb

@@ -110,13 +110,16 @@ package body System.Tasking is
          return;
       end if;
 
-      --  Wouldn't the following be better done using an assignment of an
-      --  aggregate so that we could be sure no components were forgotten???
-
       T.Common.Parent                   := Parent;
       T.Common.Base_Priority            := Base_Priority;
       T.Common.Base_CPU                 := Base_CPU;
-      T.Common.Domain                   := Domain;
+
+      --  The Domain defaults to that of the activator
+
+      T.Common.Domain                   :=
+        (if Domain = null then Self_ID.Common.Domain else Domain);
+      pragma Assert (T.Common.Domain /= null);
+
       T.Common.Current_Priority         := 0;
       T.Common.Protected_Action_Nesting := 0;
       T.Common.Call                     := null;
@@ -218,18 +221,18 @@ package body System.Tasking is
 
       T := STPO.New_ATCB (0);
       Initialize_ATCB
-        (Self_ID => null,
+        (Self_ID          => null,
          Task_Entry_Point => null,
-         Task_Arg => Null_Address,
+         Task_Arg         => Null_Address,
-         Parent => Null_Task,
+         Parent           => Null_Task,
-         Elaborated => null,
+         Elaborated       => null,
-         Base_Priority => Base_Priority,
+         Base_Priority    => Base_Priority,
-         Base_CPU => Base_CPU,
+         Base_CPU         => Base_CPU,
-         Domain => System_Domain,
+         Domain           => System_Domain,
-         Task_Info => Task_Info.Unspecified_Task_Info,
+         Task_Info        => Task_Info.Unspecified_Task_Info,
-         Stack_Size => 0,
+         Stack_Size       => 0,
-         T => T,
+         T                => T,
-         Success => Success);
+         Success          => Success);
       pragma Assert (Success);
 
       STPO.Initialize (T);

gcc/ada/s-taskin.ads

@@ -504,7 +504,7 @@ package System.Tasking is
 
    --  Section used by all GNARL implementations (regular and restricted)
 
-   type Common_ATCB is record
+   type Common_ATCB is limited record
       State : Task_States;
       pragma Atomic (State);
       --  Encodes some basic information about the state of a task,
@@ -721,7 +721,7 @@ package System.Tasking is
    --  present in the Restricted_Ada_Task_Control_Block structure.
 
    type Restricted_Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is
-   record
+   limited record
       Common : Common_ATCB;
       --  The common part between various tasking implementations
 
@@ -954,7 +954,7 @@ package System.Tasking is
    --  than 64-bits explicitly to allow codepeer to analyze this unit when
    --  a target configuration file forces the maximum integer size to 32.
 
-   type Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is record
+   type Ada_Task_Control_Block (Entry_Num : Task_Entry_Index) is limited record
       Common : Common_ATCB;
       --  The common part between various tasking implementations
 
@@ -1179,10 +1179,9 @@ package System.Tasking is
       T                : Task_Id;
       Success          : out Boolean);
    --  Initialize fields of the TCB for task T, and link into global TCB
-   --  structures. Call this only with abort deferred and holding
+   --  structures. Call this only with abort deferred and holding RTS_Lock.
-   --  RTS_Lock. Self_ID is the calling task (normally the activator of
+   --  Self_ID is the calling task (normally the activator of T). Success is
-   --  T). Success is set to indicate whether the TCB was successfully
+   --  set to indicate whether the TCB was successfully initialized.
-   --  initialized. Need more documentation ???
 
 private
 

gcc/ada/s-taspri-dummy.ads

@@ -46,7 +46,7 @@ package System.Task_Primitives is
 
    type Task_Body_Access is access procedure;
 
-   type Private_Data is record
+   type Private_Data is limited record
       Thread : aliased Integer;
       CV     : aliased Integer;
       L      : aliased RTS_Lock;

gcc/ada/s-taspri-mingw.ads

@@ -97,7 +97,7 @@ private
       --  Condition variable used to queue threads until condition is signaled
    end record;
 
-   type Private_Data is record
+   type Private_Data is limited record
       Thread : aliased Win32.HANDLE;
       pragma Atomic (Thread);
       --  Thread field may be updated by two different threads of control.

gcc/ada/s-taspri-posix-noaltstack.ads

@@ -97,7 +97,7 @@ private
       --  Condition variable used to queue threads until condition is signaled
    end record;
 
-   type Private_Data is record
+   type Private_Data is limited record
       Thread : aliased System.OS_Interface.pthread_t;
       pragma Atomic (Thread);
       --  Thread field may be updated by two different threads of control.

gcc/ada/s-taspri-posix.ads

@@ -96,7 +96,7 @@ private
       --  Condition variable used to queue threads until condition is signaled
    end record;
 
-   type Private_Data is record
+   type Private_Data is limited record
       Thread : aliased System.OS_Interface.pthread_t;
       pragma Atomic (Thread);
       --  Thread field may be updated by two different threads of control.

gcc/ada/s-taspri-solaris.ads

@@ -124,7 +124,7 @@ private
    --  Note that task support on gdb relies on the fact that the first two
    --  fields of Private_Data are Thread and LWP.
 
-   type Private_Data is record
+   type Private_Data is limited record
       Thread : aliased System.OS_Interface.thread_t;
       pragma Atomic (Thread);
       --  Thread field may be updated by two different threads of control.

gcc/ada/s-taspri-vxworks.ads

@@ -98,7 +98,7 @@ private
       --  Condition variable used to queue threads until condition is signaled
    end record;
 
-   type Private_Data is record
+   type Private_Data is limited record
       Thread : aliased System.OS_Interface.t_id := 0;
       pragma Atomic (Thread);
       --  Thread field may be updated by two different threads of control.

gcc/ada/s-tassta.adb

@@ -662,18 +662,6 @@ package body System.Tasking.Stages is
          T.Common.Task_Image_Len := Len;
       end if;
 
-      --  The task inherits the dispatching domain of the parent only if no
-      --  specific domain has been defined in the spec of the task (using the
-      --  dispatching domain pragma or aspect).
-
-      if T.Common.Domain /= null then
-         null;
-      elsif T.Common.Activator /= null then
-         T.Common.Domain := T.Common.Activator.Common.Domain;
-      else
-         T.Common.Domain := System.Tasking.System_Domain;
-      end if;
-
       Unlock (Self_ID);
       Unlock_RTS;
 

gcc/ada/sem_prag.adb

@@ -13125,7 +13125,9 @@ package body Sem_Prag is
             Citem : Node_Id;
 
          begin
-            SPARK_Msg_N ("pragma Elaborate not allowed", N);
+            if SPARK_Mode = On then
+               Error_Msg_N ("pragma Elaborate not allowed in SPARK mode", N);
+            end if;
 
             --  Pragma must be in context items list of a compilation unit
 
@@ -13207,7 +13209,15 @@ package body Sem_Prag is
             --  Give a warning if operating in static mode with one of the
             --  gnatwl/-gnatwE (elaboration warnings enabled) switches set.
 
-            if Elab_Warnings and not Dynamic_Elaboration_Checks then
+            if Elab_Warnings
+                 and not Dynamic_Elaboration_Checks
+
+                 --  pragma Elaborate not allowed in SPARK mode anyway. We
+                 --  already complained about it, no point in generating any
+                 --  further complaint.
+
+                 and SPARK_Mode /= On
+            then
                Error_Msg_N
                  ("?l?use of pragma Elaborate may not be safe", N);
                Error_Msg_N
@@ -13343,8 +13353,13 @@ package body Sem_Prag is
             GNAT_Pragma;
             Check_Arg_Count (1);
             Check_Arg_Is_One_Of (Arg1, Name_Static, Name_Dynamic);
+
+            --  Set flag accordingly (ignore attempt at dynamic elaboration
+            --  checks in SPARK mode).
+
             Dynamic_Elaboration_Checks :=
-              (Chars (Get_Pragma_Arg (Arg1)) = Name_Dynamic);
+              (Chars (Get_Pragma_Arg (Arg1)) = Name_Dynamic)
+                and then SPARK_Mode /= On;
 
          ---------------
          -- Eliminate --
@@ -19541,6 +19556,8 @@ package body Sem_Prag is
          --  pragma SPARK_Mode [(On | Off)];
 
          when Pragma_SPARK_Mode => Do_SPARK_Mode : declare
+            Mode_Id : SPARK_Mode_Type;
+
             procedure Check_Pragma_Conformance
               (Context_Pragma : Node_Id;
                Entity_Pragma  : Node_Id;
@@ -19565,6 +19582,11 @@ package body Sem_Prag is
             procedure Check_Library_Level_Entity (E : Entity_Id);
             --  Verify that pragma is applied to library-level entity E
 
+            procedure Set_SPARK_Flags;
+            --  Sets SPARK_Mode from Mode_Id and SPARK_Mode_Pragma from N,
+            --  and ensures that Dynamic_Elaboration_Checks are off if the
+            --  call sets SPARK_Mode On.
+
             ------------------------------
             -- Check_Pragma_Conformance --
             ------------------------------
@@ -19642,12 +19664,25 @@ package body Sem_Prag is
                end if;
             end Check_Library_Level_Entity;
 
+            ---------------------
+            -- Set_SPARK_Flags --
+            ---------------------
+
+            procedure Set_SPARK_Flags is
+            begin
+               SPARK_Mode := Mode_Id;
+               SPARK_Mode_Pragma := N;
+
+               if SPARK_Mode = On then
+                  Dynamic_Elaboration_Checks := False;
+               end if;
+            end Set_SPARK_Flags;
+
             --  Local variables
 
             Body_Id : Entity_Id;
             Context : Node_Id;
             Mode    : Name_Id;
-            Mode_Id : SPARK_Mode_Type;
             Spec_Id : Entity_Id;
             Stmt    : Node_Id;
 
@@ -19691,8 +19726,7 @@ package body Sem_Prag is
                   raise Pragma_Exit;
                end if;
 
-               SPARK_Mode_Pragma := N;
+               Set_SPARK_Flags;
-               SPARK_Mode := Mode_Id;
 
             --  The pragma acts as a configuration pragma in a compilation unit
 
@@ -19703,8 +19737,7 @@ package body Sem_Prag is
               and then List_Containing (N) = Context_Items (Context)
             then
                Check_Valid_Configuration_Pragma;
-               SPARK_Mode_Pragma := N;
+               Set_SPARK_Flags;
-               SPARK_Mode := Mode_Id;
 
             --  Otherwise the placement of the pragma within the tree dictates
             --  its associated construct. Inspect the declarative list where
@@ -19789,8 +19822,7 @@ package body Sem_Prag is
                        (Context_Pragma => SPARK_Pragma (Spec_Id),
                         Entity_Pragma  => Empty,
                         Entity         => Empty);
-                     SPARK_Mode_Pragma := N;
+                     Set_SPARK_Flags;
-                     SPARK_Mode := Mode_Id;
 
                      Set_SPARK_Pragma               (Spec_Id, N);
                      Set_SPARK_Pragma_Inherited     (Spec_Id, False);
@@ -19808,8 +19840,7 @@ package body Sem_Prag is
                        (Context_Pragma => Empty,
                         Entity_Pragma  => SPARK_Pragma (Spec_Id),
                         Entity         => Spec_Id);
-                     SPARK_Mode_Pragma := N;
+                     Set_SPARK_Flags;
-                     SPARK_Mode := Mode_Id;
 
                      Set_SPARK_Aux_Pragma           (Spec_Id, N);
                      Set_SPARK_Aux_Pragma_Inherited (Spec_Id, False);
@@ -19828,8 +19859,7 @@ package body Sem_Prag is
                     (Context_Pragma => SPARK_Pragma (Body_Id),
                      Entity_Pragma  => SPARK_Aux_Pragma (Spec_Id),
                      Entity         => Spec_Id);
-                  SPARK_Mode_Pragma := N;
+                  Set_SPARK_Flags;
-                  SPARK_Mode := Mode_Id;
 
                   Set_SPARK_Pragma               (Body_Id, N);
                   Set_SPARK_Pragma_Inherited     (Body_Id, False);
@@ -19853,8 +19883,7 @@ package body Sem_Prag is
                     (Context_Pragma => Empty,
                      Entity_Pragma  => SPARK_Pragma (Body_Id),
                      Entity         => Body_Id);
-                  SPARK_Mode_Pragma := N;
+                  Set_SPARK_Flags;
-                  SPARK_Mode := Mode_Id;
 
                   Set_SPARK_Aux_Pragma           (Body_Id, N);
                   Set_SPARK_Aux_Pragma_Inherited (Body_Id, False);
@@ -19916,8 +19945,7 @@ package body Sem_Prag is
                         Entity         => Empty);
                   end if;
 
-                  SPARK_Mode_Pragma := N;
+                  Set_SPARK_Flags;
-                  SPARK_Mode := Mode_Id;
 
                   Set_SPARK_Pragma           (Body_Id, N);
                   Set_SPARK_Pragma_Inherited (Body_Id, False);