[multiple changes]

2011-08-29  Yannick Moy  <moy@adacore.com>

	* sem_ch3.adb (Array_Type_Declaration): Create declarations for Itypes
	created in Alfa mode, instead of inserting artificial declarations of
	non-Itypes in the tree.
	* sem_util.adb, sem_util.ads (Itype_Has_Declaration): New function to
	know if an Itype has a corresponding declaration, as defined in
	itypes.ads.

2011-08-29  Yannick Moy  <moy@adacore.com>

	* gnat1drv.adb: Minor rewrite.

2011-08-29  Bob Duff  <duff@adacore.com>

	* s-tasuti.adb (Make_Passive): Work around race condition in
	Make_Independent, which can cause Wait_Count to be zero. So instead of
	asserting that Wait_Count > 0, and then decrementing it, decrement it
	only if Wait_Count > 0.
	* s-taskin.ads (Wait_Count, Alive_Count, Awake_Count): All of these
	should be nonnegative, so declare them Natural instead of Integer.

From-SVN: r178240

gcc/ada/ChangeLog

+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch3.adb (Array_Type_Declaration): Create declarations for Itypes
+	created in Alfa mode, instead of inserting artificial declarations of
+	non-Itypes in the tree.
+	* sem_util.adb, sem_util.ads (Itype_Has_Declaration): New function to
+	know if an Itype has a corresponding declaration, as defined in
+	itypes.ads.
+
+2011-08-29  Yannick Moy  <moy@adacore.com>
+
+	* gnat1drv.adb: Minor rewrite.
+
+2011-08-29  Bob Duff  <duff@adacore.com>
+
+	* s-tasuti.adb (Make_Passive): Work around race condition in
+	Make_Independent, which can cause Wait_Count to be zero. So instead of
+	asserting that Wait_Count > 0, and then decrementing it, decrement it
+	only if Wait_Count > 0.
+	* s-taskin.ads (Wait_Count, Alive_Count, Awake_Count): All of these
+	should be nonnegative, so declare them Natural instead of Integer.
+
 2011-08-29  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch5.adb, sem_ch3.adb, a-cihama.adb, a-cihama.ads, exp_ch7.adb,

gcc/ada/gnat1drv.adb

@@ -478,8 +478,8 @@ procedure Gnat1drv is
 
          --  We would prefer to suppress the expansion of tagged types and
          --  dispatching calls, so that one day GNATprove can handle them
-         --  directly. Unfortunately, this is causing problems on H513-015, so
-         --  keep this expansion for the time being. ???
+         --  directly. Unfortunately, this is causing problems in some cases,
+         --  so keep this expansion for the time being.
 
          Tagged_Type_Expansion := True;
       end if;

gcc/ada/s-taskin.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                  S p e c                                 --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNARL 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- --
@@ -566,7 +566,7 @@ package System.Tasking is
       --  Protection: Set by Activator before Self is activated, and only read
       --  and modified by Self after that.
 
-      Wait_Count : Integer;
+      Wait_Count : Natural;
       --  This count is used by a task that is waiting for other tasks. At all
       --  other times, the value should be zero. It is used differently in
       --  several different states. Since a task cannot be in more than one of
@@ -942,13 +942,13 @@ package System.Tasking is
       --  not write this field until the master is complete, the
       --  synchronization should be adequate to prevent races.
 
-      Alive_Count : Integer := 0;
+      Alive_Count : Natural := 0;
       --  Number of tasks directly dependent on this task (including itself)
       --  that are still "alive", i.e. not terminated.
       --
       --  Protection: Self.L
 
-      Awake_Count : Integer := 0;
+      Awake_Count : Natural := 0;
       --  Number of tasks directly dependent on this task (including itself)
       --  still "awake", i.e., are not terminated and not waiting on a
       --  terminate alternative.

gcc/ada/s-tasuti.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                  B o d y                                 --
 --                                                                          --
---         Copyright (C) 1992-2009, Free Software Foundation, Inc.          --
+--         Copyright (C) 1992-2011, Free Software Foundation, Inc.          --
 --                                                                          --
 -- GNARL 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- --
@@ -504,12 +504,14 @@ package body System.Tasking.Utilities is
            (Debug.Trace
             (Self_ID, "Make_Passive: Phase 1, parent waiting", 'M'));
 
-         --  If parent is in Master_Completion_Sleep, it
-         --  cannot be on a terminate alternative, hence
-         --  it cannot have Awake_Count of zero.
+         --  If parent is in Master_Completion_Sleep, it cannot be on a
+         --  terminate alternative, hence it cannot have Wait_Count of
+         --  zero. ???Except that the race condition in Make_Independent can
+         --  cause Wait_Count to be zero, so we need to check for that.
 
-         pragma Assert (P.Common.Wait_Count > 0);
-         P.Common.Wait_Count := P.Common.Wait_Count - 1;
+         if P.Common.Wait_Count > 0 then
+            P.Common.Wait_Count := P.Common.Wait_Count - 1;
+         end if;
 
          if P.Common.Wait_Count = 0 then
             Wakeup (P, Master_Completion_Sleep);

gcc/ada/sem_ch3.adb

@@ -4741,26 +4741,20 @@ package body Sem_Ch3 is
 
          Make_Index (Index, P, Related_Id, Nb_Index);
 
-         --  In formal verification mode, create an explicit subtype for every
-         --  index if not already a subtype_mark, and replace the existing type
-         --  of index by this new type. Having a declaration for all type
+         --  In formal verification mode, create an explicit declaration for
+         --  Itypes created for index types. Having a declaration for all type
          --  entities facilitates the task of the formal verification back-end.
+         --  Notice that this declaration is not attached to the tree.
 
          if ALFA_Mode
-           and then not Nkind_In (Index, N_Identifier, N_Expanded_Name)
+           and then Is_Itype (Etype (Index))
          then
             declare
                Loc     : constant Source_Ptr := Sloc (Def);
-               New_E   : Entity_Id;
-               Decl    : Entity_Id;
                Sub_Ind : Node_Id;
+               Decl    : Entity_Id;
 
             begin
-               New_E :=
-                 New_External_Entity
-                   (E_Void, Current_Scope, Sloc (P), Related_Id, 'D',
-                    Nb_Index, 'T');
-
                if Nkind (Index) = N_Subtype_Indication then
                   Sub_Ind := Relocate_Node (Index);
                else
@@ -4775,11 +4769,10 @@ package body Sem_Ch3 is
 
                Decl :=
                  Make_Subtype_Declaration (Loc,
-                   Defining_Identifier => New_E,
+                   Defining_Identifier => Etype (Index),
                    Subtype_Indication  => Sub_Ind);
 
-               Insert_Action (Parent (Def), Decl);
-               Set_Etype (Index, New_E);
+               Analyze (Decl);
             end;
          end if;
 
@@ -4799,34 +4792,29 @@ package body Sem_Ch3 is
 
       if Present (Component_Typ) then
 
-         --  In formal verification mode, create an explicit subtype for the
-         --  component type if not already a subtype_mark. Having a declaration
-         --  for all type entities facilitates the task of the formal
-         --  verification back-end.
+         Element_Type := Process_Subtype (Component_Typ, P, Related_Id, 'C');
+
+         --  In formal verification mode, create an explicit declaration for
+         --  the Itype created for a component type. Having a declaration for
+         --  all type entities facilitates the task of the formal verification
+         --  back-end. Notice that this declaration is not attached to the
+         --  tree.
 
          if ALFA_Mode
-           and then Nkind (Component_Typ) = N_Subtype_Indication
+           and then Is_Itype (Element_Type)
          then
             declare
                Loc  : constant Source_Ptr := Sloc (Def);
                Decl : Entity_Id;
 
             begin
-               Element_Type :=
-                 New_External_Entity
-                   (E_Void, Current_Scope, Sloc (P), Related_Id, 'C', 0, 'T');
-
                Decl :=
                  Make_Subtype_Declaration (Loc,
                    Defining_Identifier => Element_Type,
                    Subtype_Indication  => Relocate_Node (Component_Typ));
 
-               Insert_Action (Parent (Def), Decl);
+               Analyze (Decl);
             end;
-
-         else
-            Element_Type :=
-              Process_Subtype (Component_Typ, P, Related_Id, 'C');
          end if;
 
          Set_Etype (Component_Typ, Element_Type);
@@ -4915,6 +4903,30 @@ package body Sem_Ch3 is
                                (Implicit_Base, Finalize_Storage_Only
                                                         (Element_Type));
 
+         --  In ALFA mode, generate a declaration for Itype T, so that the
+         --  formal verification back-end can use it.
+
+         if ALFA_Mode
+           and then Is_Itype (T)
+         then
+            declare
+               Loc  : constant Source_Ptr := Sloc (Def);
+               Decl : Node_Id;
+
+            begin
+               Decl := Make_Full_Type_Declaration (Loc,
+                  Defining_Identifier => T,
+                  Type_Definition     =>
+                   Make_Constrained_Array_Definition (Loc,
+                     Discrete_Subtype_Definitions =>
+                       New_Copy_List (Discrete_Subtype_Definitions (Def)),
+                     Component_Definition         =>
+                       Relocate_Node (Component_Definition (Def))));
+
+               Analyze (Decl);
+            end;
+         end if;
+
       --  Unconstrained array case
 
       else

gcc/ada/sem_util.adb

@@ -8507,6 +8507,20 @@ package body Sem_Util is
       end if;
    end Is_Volatile_Object;
 
+   ---------------------------
+   -- Itype_Has_Declaration --
+   ---------------------------
+
+   function Itype_Has_Declaration (Id : Entity_Id) return Boolean is
+   begin
+      pragma Assert (Is_Itype (Id));
+      return Present (Parent (Id))
+        and then Nkind_In (Parent (Id),
+                           N_Full_Type_Declaration,
+                           N_Subtype_Declaration)
+        and then Defining_Entity (Parent (Id)) = Id;
+   end Itype_Has_Declaration;
+
    -------------------------
    -- Kill_Current_Values --
    -------------------------

gcc/ada/sem_util.ads

@@ -969,6 +969,11 @@ package Sem_Util is
    --  for something actually declared as volatile, not for an object that gets
    --  treated as volatile (see Einfo.Treat_As_Volatile).
 
+   function Itype_Has_Declaration (Id : Entity_Id) return Boolean;
+   --  Applies to Itypes. True if the Itype is attached to a declaration for
+   --  the type through its Parent field, which may or not be present in the
+   --  tree.
+
    procedure Kill_Current_Values (Last_Assignment_Only : Boolean := False);
    --  This procedure is called to clear all constant indications from all
    --  entities in the current scope and in any parent scopes if the current