[multiple changes]

2014-01-20  Arnaud Charlet  <charlet@adacore.com>

	* s-tataat.adb (Initialize_Attributes): Abort might already be
	deferred in Create_Task.

2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* checks.adb (Apply_Scalar_Range_Check): Flag
	the exponent as requiring a range check when the expression is
	an exponentiation.

From-SVN: r206831

gcc/ada/ChangeLog

+2014-01-20  Arnaud Charlet  <charlet@adacore.com>
+
+	* s-tataat.adb (Initialize_Attributes): Abort might already be
+	deferred in Create_Task.
+
+2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* checks.adb (Apply_Scalar_Range_Check): Flag
+	the exponent as requiring a range check when the expression is
+	an exponentiation.
+
 2014-01-20  Fedor Rybin  <frybin@adacore.com>
 
 	* gnat_ugn.texi: Documenting --passed-tests option for gnattest.

gcc/ada/checks.adb

@@ -2797,6 +2797,19 @@ package body Checks is
          return;
       end if;
 
+      --  Ensure that the exponent is a natural. The flag is set only in formal
+      --  verification mode as the expander takes care of this check and there
+      --  is no expansion phase in GNATprove_Mode.
+
+      --  Doesn't seem right to do this unconditionally, we should check the
+      --  range of the exponent operand. If we do that, it seems like we should
+      --  then set the flag unconditionally and have the expander check the
+      --  flag to see whether to generate a check ???
+
+      if GNATprove_Mode and then Nkind (Expr) = N_Op_Expon then
+         Set_Do_Range_Check (Right_Opnd (Expr));
+      end if;
+
       Is_Unconstrained_Subscr_Ref :=
         Is_Subscr_Ref and then not Is_Constrained (Arr_Typ);
 

gcc/ada/s-tataat.adb

@@ -7,7 +7,7 @@
 --                                  B o d y                                 --
 --                                                                          --
 --             Copyright (C) 1991-1994, Florida State University            --
---                     Copyright (C) 1995-2010, AdaCore                     --
+--                     Copyright (C) 1995-2013, AdaCore                     --
 --                                                                          --
 -- 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- --
@@ -186,7 +186,7 @@ package body System.Tasking.Task_Attributes is
       Self_Id : constant Task_Id := Self;
 
    begin
-      Defer_Abort (Self_Id);
+      Defer_Abort_Nestable (Self_Id);
       Lock_RTS;
 
       --  Initialize all the direct-access attributes of this task
@@ -204,7 +204,7 @@ package body System.Tasking.Task_Attributes is
       end loop;
 
       Unlock_RTS;
-      Undefer_Abort (Self_Id);
+      Undefer_Abort_Nestable (Self_Id);
 
    exception
       when others =>