[multiple changes]

2012-10-05  Yannick Moy  <moy@adacore.com>

	* switch-c.adb, checks.adb, checks.ads, sem_prag.adb, exp_ch4.adb,
	osint.adb: Minor correction of typos, and special case for Alfa mode.

2012-10-05  Hristian Kirtchev  <kirtchev@adacore.com>

	* s-spsufi.adb: Add with clause for Ada.Unchecked_Deallocation.
	Add with and use clauses for System.Finalization_Masters.
	(Finalize_And_Deallocate): Add an instance of
	Ada.Unchecked_Deallocation. Merge the code from the now obsolete
	Finalize_Subpool into this routine.
	* s-spsufi.ads: Add pragma Preelaborate.
	* s-stposu.adb: Remove with clause for
	Ada.Unchecked_Deallocation; Add with and use clauses for
	System.Storage_Pools.Subpools.Finalization; (Finalize_Pool):
	Update the comment on all actions takes with respect to a subpool
	finalization. Finalize and deallocate each individual subpool.
	(Finalize_Subpool): Removed.
	(Free): Removed;
	(Detach): Move from package body to spec.
	* s-stposu.ads (Detach): Move from package body to spec.
	(Finalize_Subpool): Removed.

2012-10-05  Arnaud Charlet  <charlet@adacore.com>

	* s-tassta.adb: Update comments.
	(Vulnerable_Complete_Master): If Free_On_Termination is set, do
	nothing, and let the task free itself if not already done.

From-SVN: r192124

gcc/ada/ChangeLog

+2012-10-05  Yannick Moy  <moy@adacore.com>
+
+	* switch-c.adb, checks.adb, checks.ads, sem_prag.adb, exp_ch4.adb,
+	osint.adb: Minor correction of typos, and special case for Alfa mode.
+
+2012-10-05  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* s-spsufi.adb: Add with clause for Ada.Unchecked_Deallocation.
+	Add with and use clauses for System.Finalization_Masters.
+	(Finalize_And_Deallocate): Add an instance of
+	Ada.Unchecked_Deallocation. Merge the code from the now obsolete
+	Finalize_Subpool into this routine.
+	* s-spsufi.ads: Add pragma Preelaborate.
+	* s-stposu.adb: Remove with clause for
+	Ada.Unchecked_Deallocation; Add with and use clauses for
+	System.Storage_Pools.Subpools.Finalization; (Finalize_Pool):
+	Update the comment on all actions takes with respect to a subpool
+	finalization. Finalize and deallocate each individual subpool.
+	(Finalize_Subpool): Removed.
+	(Free): Removed;
+	(Detach): Move from package body to spec.
+	* s-stposu.ads (Detach): Move from package body to spec.
+	(Finalize_Subpool): Removed.
+
+2012-10-05  Arnaud Charlet  <charlet@adacore.com>
+
+	* s-tassta.adb: Update comments.
+	(Vulnerable_Complete_Master): If Free_On_Termination is set, do
+	nothing, and let the task free itself if not already done.
+
 2012-10-04  Robert Dewar  <dewar@adacore.com>
 
 	* sem_res.adb (Resolve_Set_Membership): Warn on duplicates.

gcc/ada/checks.ads

@@ -223,7 +223,7 @@ package Checks is
    --  Returns result of converting node N to Bignum. The returned value is not
    --  analyzed, the caller takes responsibility for this. Node N must be a
    --  subexpression node of a signed integer type or Bignum type (if it is
-   --  already a Bignnum, the returned value is Relocate_Node (N).
+   --  already a Bignum, the returned value is Relocate_Node (N)).
 
    procedure Determine_Range
      (N            : Node_Id;
@@ -273,7 +273,7 @@ package Checks is
       Top_Level : Boolean);
    --  This is the main routine for handling MINIMIZED and ELIMINATED overflow
    --  checks. On entry N is a node whose result is a signed integer subtype.
-   --  If the node is an artihmetic operation, then a range analysis is carried
+   --  If the node is an arithmetic operation, then a range analysis is carried
    --  out, and there are three possibilities:
    --
    --    The node is left unchanged (apart from expansion of an exponentiation
@@ -289,13 +289,13 @@ package Checks is
    --
    --  In the first two cases, Lo and Hi are set to the bounds of the possible
    --  range of results, computed as accurately as possible. In the third case
-   --  Lo and Hi are set to No_Uint (there are some cases where we cold get an
+   --  Lo and Hi are set to No_Uint (there are some cases where we could get an
    --  advantage from keeping result ranges for Bignum values, but it could use
    --  a lot of space and is very unlikely to be valuable).
    --
    --  If the node is not an arithmetic operation, then it is unchanged but
    --  Lo and Hi are still set (to the bounds of the result subtype if nothing
-   --  better can be determined.
+   --  better can be determined).
    --
    --  Note: this function is recursive, if called with an arithmetic operator,
    --  recursive calls are made to process the operands using this procedure.
@@ -310,8 +310,8 @@ package Checks is
    --  with a Long_Long_Integer left operand and an Integer right operand, and
    --  we would get a semantic error.
    --
-   --  The routine is called in three situations if we are operating in
-   --  either MINIMIZED or ELIMINATED modes.
+   --  The routine is called in three situations if we are operating in either
+   --  MINIMIZED or ELIMINATED modes.
    --
    --    Overflow checks applied to the top node of an expression tree when
    --    that node is an arithmetic operator. In this case the result is
@@ -320,7 +320,7 @@ package Checks is
    --
    --    Overflow checks are applied to the operands of a comparison operation.
    --    In this case, the comparison is done on the result Long_Long_Integer
-   --    or Bignum values, without raising any exceptions.
+   --    or Bignum values, without raising any exception.
    --
    --    Overflow checks are applied to the left operand of a membership test.
    --    In this case no exception is raised if a Long_Long_Integer or Bignum
@@ -328,7 +328,7 @@ package Checks is
    --    just that the result of IN is false in that case).
    --
    --  Note that if Bignum values appear, the caller must take care of doing
-   --  the appropriate mark/release operation on the secondary stack.
+   --  the appropriate mark/release operations on the secondary stack.
    --
    --  Top_Level is used to avoid inefficient unnecessary transitions into the
    --  Bignum domain. If Top_Level is True, it means that the caller will have

gcc/ada/exp_ch4.adb

@@ -141,8 +141,8 @@ package body Exp_Ch4 is
    --  Common expansion processing for short-circuit boolean operators
 
    procedure Expand_Compare_Minimize_Eliminate_Overflow (N : Node_Id);
-   --  Deal with comparison in Minimize/Eliminate overflow mode. This is where
-   --  we allow comparison of "out of range" values.
+   --  Deal with comparison in MINIMIZED/ELIMINATED overflow mode. This is
+   --  where we allow comparison of "out of range" values.
 
    function Expand_Composite_Equality
      (Nod    : Node_Id;
@@ -165,10 +165,10 @@ package body Exp_Ch4 is
    --  include both arrays and singleton elements.
 
    procedure Expand_Membership_Minimize_Eliminate_Overflow (N : Node_Id);
-   --  N is an N_In membership test mode, with the overflow check mode
-   --  set to Minimized or Eliminated, and the type of the left operand
-   --  is a signed integer type. This is a case where top level processing
-   --  is required to handle overflow checks in subtrees.
+   --  N is an N_In membership test mode, with the overflow check mode set to
+   --  MINIMIZED or ELIMINATED, and the type of the left operand is a signed
+   --  integer type. This is a case where top level processing is required to
+   --  handle overflow checks in subtrees.
 
    procedure Fixup_Universal_Fixed_Operation (N : Node_Id);
    --  N is a N_Op_Divide or N_Op_Multiply node whose result is universal
@@ -5524,7 +5524,7 @@ package body Exp_Ch4 is
       Ltyp := Etype (Left_Opnd  (N));
       Rtyp := Etype (Right_Opnd (N));
 
-      --  If Minimize/Eliminate overflow mode and type is a signed integer
+      --  If MINIMIZED/ELIMINATED overflow mode and type is a signed integer
       --  type, then expand with a separate procedure. Note the use of the
       --  flag No_Minimize_Eliminate to prevent infinite recursion.
 
@@ -7084,7 +7084,7 @@ package body Exp_Ch4 is
       Typl := Base_Type (Typl);
 
       --  Deal with overflow checks in MINIMIZED/ELIMINATED mode and if that
-      --  results in not having a comparison operation any more, we are done.
+      --  results in not having a comparison operation anymore, we are done.
 
       Expand_Compare_Minimize_Eliminate_Overflow (N);
 
@@ -7678,7 +7678,7 @@ package body Exp_Ch4 is
       Binary_Op_Validity_Checks (N);
 
       --  Deal with overflow checks in MINIMIZED/ELIMINATED mode and if that
-      --  results in not having a comparison operation any more, we are done.
+      --  results in not having a comparison operation anymore, we are done.
 
       Expand_Compare_Minimize_Eliminate_Overflow (N);
 
@@ -7728,7 +7728,7 @@ package body Exp_Ch4 is
       Binary_Op_Validity_Checks (N);
 
       --  Deal with overflow checks in MINIMIZED/ELIMINATED mode and if that
-      --  results in not having a comparison operation any more, we are done.
+      --  results in not having a comparison operation anymore, we are done.
 
       Expand_Compare_Minimize_Eliminate_Overflow (N);
 
@@ -7778,7 +7778,7 @@ package body Exp_Ch4 is
       Binary_Op_Validity_Checks (N);
 
       --  Deal with overflow checks in MINIMIZED/ELIMINATED mode and if that
-      --  results in not having a comparison operation any more, we are done.
+      --  results in not having a comparison operation anymore, we are done.
 
       Expand_Compare_Minimize_Eliminate_Overflow (N);
 
@@ -7828,7 +7828,7 @@ package body Exp_Ch4 is
       Binary_Op_Validity_Checks (N);
 
       --  Deal with overflow checks in MINIMIZED/ELIMINATED mode and if that
-      --  results in not having a comparison operation any more, we are done.
+      --  results in not having a comparison operation anymore, we are done.
 
       Expand_Compare_Minimize_Eliminate_Overflow (N);
 
@@ -8263,7 +8263,7 @@ package body Exp_Ch4 is
          Binary_Op_Validity_Checks (N);
 
          --  Deal with overflow checks in MINIMIZED/ELIMINATED mode and if
-         --  that results in not having a /= opertion any more, we are done.
+         --  that results in not having a /= operation anymore, we are done.
 
          Expand_Compare_Minimize_Eliminate_Overflow (N);
 

gcc/ada/osint.adb

@@ -1658,7 +1658,7 @@ package body Osint is
       --  Start off by setting all suppress options, to False. The special
       --  overflow fields are set to Not_Set (they will be set by -gnatp, or
       --  by -gnato, or, if neither of these appear, in Adjust_Global_Switches
-      --  in Gnat1drv.
+      --  in Gnat1drv).
 
       Suppress_Options := ((others => False), Not_Set, Not_Set);
 

gcc/ada/s-spsufi.adb

@@ -7,7 +7,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---             Copyright (C) 2011, Free Software Foundation, Inc.           --
+--           Copyright (C) 2011-2012, 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- --
@@ -30,6 +30,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+with Ada.Unchecked_Deallocation;
+with System.Finalization_Masters; use System.Finalization_Masters;
+
 package body System.Storage_Pools.Subpools.Finalization is
 
    -----------------------------
@@ -37,6 +40,8 @@ package body System.Storage_Pools.Subpools.Finalization is
    -----------------------------
 
    procedure Finalize_And_Deallocate (Subpool : in out Subpool_Handle) is
+      procedure Free is new Ada.Unchecked_Deallocation (SP_Node, SP_Node_Ptr);
+
    begin
       --  Do nothing if the subpool was never created or never used. The latter
       --  case may arise with an array of subpool implementations.
@@ -48,9 +53,18 @@ package body System.Storage_Pools.Subpools.Finalization is
          return;
       end if;
 
-      --  Clean up all controlled objects allocated through the subpool
+      --  Clean up all controlled objects chained on the subpool's master
+
+      Finalize (Subpool.Master);
+
+      --  Remove the subpool from its owner's list of subpools
+
+      Detach (Subpool.Node);
+
+      --  Destroy the associated doubly linked list node which was created in
+      --  Set_Pool_Of_Subpools.
 
-      Finalize_Subpool (Subpool);
+      Free (Subpool.Node);
 
       --  Dispatch to the user-defined implementation of Deallocate_Subpool
 

gcc/ada/s-spsufi.ads

@@ -7,7 +7,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---             Copyright (C) 2011, Free Software Foundation, Inc.           --
+--           Copyright (C) 2011-2012, 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- --
@@ -33,6 +33,7 @@
 pragma Compiler_Unit;
 
 package System.Storage_Pools.Subpools.Finalization is
+   pragma Preelaborate;
 
    procedure Finalize_And_Deallocate (Subpool : in out Subpool_Handle);
    --  This routine performs the following actions:

gcc/ada/s-stposu.adb

@@ -31,12 +31,13 @@
 
 with Ada.Exceptions;              use Ada.Exceptions;
 with Ada.Unchecked_Conversion;
-with Ada.Unchecked_Deallocation;
 with System.Address_Image;
 with System.Finalization_Masters; use System.Finalization_Masters;
 with System.IO;                   use System.IO;
 with System.Soft_Links;           use System.Soft_Links;
 with System.Storage_Elements;     use System.Storage_Elements;
+with System.Storage_Pools.Subpools.Finalization;
+use  System.Storage_Pools.Subpools.Finalization;
 
 package body System.Storage_Pools.Subpools is
 
@@ -51,11 +52,6 @@ package body System.Storage_Pools.Subpools is
    procedure Attach (N : not null SP_Node_Ptr; L : not null SP_Node_Ptr);
    --  Attach a subpool node to a pool
 
-   procedure Free is new Ada.Unchecked_Deallocation (SP_Node, SP_Node_Ptr);
-
-   procedure Detach (N : not null SP_Node_Ptr);
-   --  Unhook a subpool node from an arbitrary subpool list
-
    -----------------------------------
    -- Adjust_Controlled_Dereference --
    -----------------------------------
@@ -544,9 +540,10 @@ package body System.Storage_Pools.Subpools is
          --    2) Remove the the subpool from the owner's list of subpools
          --    3) Deallocate the doubly linked list node associated with the
          --       subpool.
+         --    4) Call Deallocate_Subpool
 
          begin
-            Finalize_Subpool (Curr_Ptr.Subpool);
+            Finalize_And_Deallocate (Curr_Ptr.Subpool);
 
          exception
             when Fin_Occur : others =>
@@ -565,32 +562,6 @@ package body System.Storage_Pools.Subpools is
       end if;
    end Finalize_Pool;
 
-   ----------------------
-   -- Finalize_Subpool --
-   ----------------------
-
-   procedure Finalize_Subpool (Subpool : not null Subpool_Handle) is
-   begin
-      --  Do nothing if the subpool was never used
-
-      if Subpool.Owner = null or else Subpool.Node = null then
-         return;
-      end if;
-
-      --  Clean up all controlled objects chained on the subpool's master
-
-      Finalize (Subpool.Master);
-
-      --  Remove the subpool from its owner's list of subpools
-
-      Detach (Subpool.Node);
-
-      --  Destroy the associated doubly linked list node which was created in
-      --  Set_Pool_Of_Subpool.
-
-      Free (Subpool.Node);
-   end Finalize_Subpool;
-
    ------------------------------
    -- Header_Size_With_Padding --
    ------------------------------

gcc/ada/s-stposu.ads

@@ -325,6 +325,9 @@ private
    --    is controlled. When set to True, the machinery generates additional
    --    data.
 
+   procedure Detach (N : not null SP_Node_Ptr);
+   --  Unhook a subpool node from an arbitrary subpool list
+
    overriding procedure Finalize (Controller : in out Pool_Controller);
    --  Buffer routine, calls Finalize_Pool
 
@@ -333,11 +336,6 @@ private
    --  their masters. This action first detaches a controlled object from a
    --  particular master, then invokes its Finalize_Address primitive.
 
-   procedure Finalize_Subpool (Subpool : not null Subpool_Handle);
-   --  Finalize all controlled objects chained on Subpool's master. Remove the
-   --  subpool from its owner's list. Deallocate the associated doubly linked
-   --  list node.
-
    function Header_Size_With_Padding
      (Alignment : System.Storage_Elements.Storage_Count)
       return System.Storage_Elements.Storage_Count;

gcc/ada/s-tassta.adb

@@ -1905,7 +1905,16 @@ package body System.Tasking.Stages is
       C := All_Tasks_List;
       P := null;
       while C /= null loop
-         if C.Common.Parent = Self_ID and then C.Master_of_Task >= CM then
+         --  If Free_On_Termination is set, do nothing here, and let
+         --  the task free itself if not already done, otherwise we
+         --  risk a race condition where Vulnerable_Free_Task is called
+         --  in the loop below, while the task calls Free_Task itself,
+         --  in Terminate_Task.
+
+         if C.Common.Parent = Self_ID
+           and then C.Master_of_Task >= CM
+           and then not C.Free_On_Termination
+         then
             if P /= null then
                P.Common.All_Tasks_Link := C.Common.All_Tasks_Link;
             else
@@ -2088,9 +2097,7 @@ package body System.Tasking.Stages is
    --  is called from Expunge_Unactivated_Tasks.
 
    --  For tasks created by elaboration of task object declarations it is
-   --  called from the finalization code of the Task_Wrapper procedure. It is
-   --  also called from Ada.Unchecked_Deallocation, for objects that are or
-   --  contain tasks.
+   --  called from the finalization code of the Task_Wrapper procedure.
 
    procedure Vulnerable_Free_Task (T : Task_Id) is
    begin

gcc/ada/sem_prag.adb

@@ -11798,8 +11798,16 @@ package body Sem_Prag is
                Check_Optional_Identifier (Arg, Name);
                Check_Arg_Is_Identifier (Argx);
 
+               --  Do not suppress overflow checks for formal verification.
+               --  Instead, require that a check is inserted so that formal
+               --  verification can detect wraparound errors.
+
                if Chars (Argx) = Name_Suppressed then
-                  return Suppressed;
+                  if Alfa_Mode then
+                     return Checked;
+                  else
+                     return Suppressed;
+                  end if;
 
                elsif Chars (Argx) = Name_Checked then
                   return Checked;

gcc/ada/switch-c.adb

@@ -53,7 +53,7 @@ package body Switch.C is
 
    function Get_Overflow_Mode (C : Character) return Overflow_Check_Type;
    --  Given a digit in the range 0 .. 3, returns the corresponding value of
-   --  Overflow_Check_Type. Raises program error if C is outside this range.
+   --  Overflow_Check_Type. Raises Program_Error if C is outside this range.
 
    function Switch_Subsequently_Cancelled
      (C        : String;
@@ -867,11 +867,11 @@ package body Switch.C is
                      then
                         Suppress_Options.Suppress (J) := True;
                      end if;
-
-                     Suppress_Options.Overflow_Checks_General    := Suppressed;
-                     Suppress_Options.Overflow_Checks_Assertions := Suppressed;
                   end loop;
 
+                  Suppress_Options.Overflow_Checks_General    := Suppressed;
+                  Suppress_Options.Overflow_Checks_Assertions := Suppressed;
+
                   Validity_Checks_On  := False;
                   Opt.Suppress_Checks := True;
                end if;