[multiple changes]

2014-07-30  Robert Dewar  <dewar@adacore.com>

	* s-tasuti.adb, s-tasuti.ads, einfo.ads, sem_prag.adb, s-taasde.adb,
	g-socthi-vms.adb, s-taprop-mingw.adb, s-interr.adb, s-interr-hwint.adb,
	g-decstr.adb, s-tasdeb-vms.adb, g-expect-vms.adb, makeutl.adb,
	s-interr-vms.adb, g-socthi.adb, exp_aggr.adb, s-tasdeb.adb,
	g-awk.adb, gnatls.adb, s-taspri-posix.ads, g-catiio.adb,
	s-interr-sigaction.adb, s-os_lib.adb, s-fileio.adb: Minor reformatting
	& code reorganization.

2014-07-30  Bob Duff  <duff@adacore.com>

	* s-tassta.adb, sem_util.ads: Minor reformatting.

2014-07-30  Yannick Moy  <moy@adacore.com>

	* inline.adb (Build_Body_To_Inline): Detect when
	subprogram has multiple returns, or not a single last return
	statement, in GNATprove mode.
	(Cannot_Inline): Simplify logic to handle case of GNATprove
	inlining first.

2014-07-30  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch6.adb: Stubs are not subject to inlining.

From-SVN: r213257

29 files changed, 156 insertions, 67 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 4eb3b01..fa02f38 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,29 @@
+2014-07-30  Robert Dewar  <dewar@adacore.com>
+
+	* s-tasuti.adb, s-tasuti.ads, einfo.ads, sem_prag.adb, s-taasde.adb,
+	g-socthi-vms.adb, s-taprop-mingw.adb, s-interr.adb, s-interr-hwint.adb,
+	g-decstr.adb, s-tasdeb-vms.adb, g-expect-vms.adb, makeutl.adb,
+	s-interr-vms.adb, g-socthi.adb, exp_aggr.adb, s-tasdeb.adb,
+	g-awk.adb, gnatls.adb, s-taspri-posix.ads, g-catiio.adb,
+	s-interr-sigaction.adb, s-os_lib.adb, s-fileio.adb: Minor reformatting
+	& code reorganization.
+
+2014-07-30  Bob Duff  <duff@adacore.com>
+
+	* s-tassta.adb, sem_util.ads: Minor reformatting.
+
+2014-07-30  Yannick Moy  <moy@adacore.com>
+
+	* inline.adb (Build_Body_To_Inline): Detect when
+	subprogram has multiple returns, or not a single last return
+	statement, in GNATprove mode.
+	(Cannot_Inline): Simplify logic to handle case of GNATprove
+	inlining first.
+
+2014-07-30  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch6.adb: Stubs are not subject to inlining.
+
 2014-07-30  Bob Duff  <duff@adacore.com>
 
 	* s-tasuti.ads, s-tasuti.adb (Make_Independent): Change this
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index 6d03646..d6f6bec 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -2476,7 +2476,7 @@ package Einfo is
 --       be compiled. Is_Inlined is also set on generic subprograms and is
 --       inherited by their instances. It is also set on the body entities
 --       of inlined subprograms. See also Has_Pragma_Inline.
-
+--
 --       Is_Inlined is also set for subprograms that are always inlined in
 --       GNATprove mode. GNATprove uses this flag to know when a body does not
 --       need to be analyzed.
diff --git a/gcc/ada/exp_aggr.adb b/gcc/ada/exp_aggr.adb
index 22b5e26..beb5f45 100644
--- a/gcc/ada/exp_aggr.adb
+++ b/gcc/ada/exp_aggr.adb
@@ -4016,6 +4016,8 @@ package body Exp_Aggr is
       --       an integer whose unsigned value is the binary concatenation of
       --       K times its remainder modulo 2**Storage_Unit.
 
+      --  What on earth does 5 mean, incomprehensible???
+
       --  The ultimate goal is to generate a call to a fast memset routine
       --  specifically optimized for the target.
 
@@ -4054,6 +4056,7 @@ package body Exp_Aggr is
             end loop;
 
             Ctyp := Component_Type (Ctyp);
+
             if Is_Atomic (Ctyp) then
                return False;
             end if;
diff --git a/gcc/ada/g-awk.adb b/gcc/ada/g-awk.adb
index f2c934c..6f58e46 100644
--- a/gcc/ada/g-awk.adb
+++ b/gcc/ada/g-awk.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 2000-2011, AdaCore                     --
+--                     Copyright (C) 2000-2014, 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- --
@@ -929,7 +929,6 @@ package body GNAT.AWK is
          if Callbacks in Only .. Pass_Through then
             declare
                Discard : Boolean;
-               pragma Unreferenced (Discard);
             begin
                Discard := Apply_Filters (Session);
             end;
diff --git a/gcc/ada/g-catiio.adb b/gcc/ada/g-catiio.adb
index 2ab7622..c0ccb4b 100644
--- a/gcc/ada/g-catiio.adb
+++ b/gcc/ada/g-catiio.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 1999-2010, AdaCore                     --
+--                     Copyright (C) 1999-2014, 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- --
@@ -789,7 +789,6 @@ package body GNAT.Calendar.Time_IO is
       else
          declare
             Discard : Second_Duration;
-            pragma Unreferenced (Discard);
          begin
             Split (Clock, Year, Month, Day, Hour, Minute, Second,
                    Sub_Second => Discard);
diff --git a/gcc/ada/g-decstr.adb b/gcc/ada/g-decstr.adb
index 255e78a..ab8d06c 100644
--- a/gcc/ada/g-decstr.adb
+++ b/gcc/ada/g-decstr.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---                     Copyright (C) 2007-2013, AdaCore                     --
+--                     Copyright (C) 2007-2014, 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- --
@@ -323,7 +323,6 @@ package body GNAT.Decode_String is
 
    procedure Next_Wide_Character (Input : String; Ptr : in out Natural) is
       Discard : Wide_Character;
-      pragma Unreferenced (Discard);
    begin
       Decode_Wide_Character (Input, Ptr, Discard);
    end Next_Wide_Character;
@@ -334,7 +333,6 @@ package body GNAT.Decode_String is
 
    procedure Next_Wide_Wide_Character (Input : String; Ptr : in out Natural) is
       Discard : Wide_Wide_Character;
-      pragma Unreferenced (Discard);
    begin
       Decode_Wide_Wide_Character (Input, Ptr, Discard);
    end Next_Wide_Wide_Character;
diff --git a/gcc/ada/g-expect-vms.adb b/gcc/ada/g-expect-vms.adb
index cbffb57..aa1f803 100644
--- a/gcc/ada/g-expect-vms.adb
+++ b/gcc/ada/g-expect-vms.adb
@@ -1111,7 +1111,6 @@ package body GNAT.Expect is
       Descriptors : Array_Of_Pd := (1 => Descriptor'Unrestricted_Access);
 
       Discard : Natural;
-      pragma Unreferenced (Discard);
 
    begin
       if Empty_Buffer then
diff --git a/gcc/ada/g-socthi-vms.adb b/gcc/ada/g-socthi-vms.adb
index 4005cd3..e2adc8c 100644
--- a/gcc/ada/g-socthi-vms.adb
+++ b/gcc/ada/g-socthi-vms.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 2001-2013, AdaCore                     --
+--                     Copyright (C) 2001-2014, 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- --
@@ -415,7 +415,6 @@ package body GNAT.Sockets.Thin is
       Val : aliased C.int := 1;
 
       Discard : C.int;
-      pragma Unreferenced (Discard);
 
    begin
       R := Syscall_Socket (Domain, Typ, Protocol);
diff --git a/gcc/ada/g-socthi.adb b/gcc/ada/g-socthi.adb
index 76d82a8..6f6fd37 100644
--- a/gcc/ada/g-socthi.adb
+++ b/gcc/ada/g-socthi.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                     Copyright (C) 2001-2013, AdaCore                     --
+--                     Copyright (C) 2001-2014, 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- --
@@ -383,7 +383,6 @@ package body GNAT.Sockets.Thin is
       Val : aliased C.int := 1;
 
       Discard : C.int;
-      pragma Unreferenced (Discard);
 
    begin
       R := Syscall_Socket (Domain, Typ, Protocol);
diff --git a/gcc/ada/gnatls.adb b/gcc/ada/gnatls.adb
index 576b41a..2fd05d9 100644
--- a/gcc/ada/gnatls.adb
+++ b/gcc/ada/gnatls.adb
@@ -1796,7 +1796,6 @@ begin
 
             declare
                Discard : ALI_Id;
-               pragma Unreferenced (Discard);
             begin
                Discard :=
                  Scan_ALI
diff --git a/gcc/ada/inline.adb b/gcc/ada/inline.adb
index 9701f3a..b9d0d8e 100644
--- a/gcc/ada/inline.adb
+++ b/gcc/ada/inline.adb
@@ -860,6 +860,11 @@ package body Inline is
       --  function. In that case the call can be replaced by that local
       --  variable as is done for other inlined calls.
 
+      function Has_Single_Return_In_GNATprove_Mode return Boolean;
+      --  This function is called only in GNATprove mode, and it returns
+      --  True if the subprogram has no or a single return statement as
+      --  last statement.
+
       procedure Remove_Pragmas;
       --  A pragma Unreferenced or pragma Unmodified that mentions a formal
       --  parameter has no meaning when the body is inlined and the formals
@@ -1143,6 +1148,57 @@ package body Inline is
          end if;
       end Has_Single_Return;
 
+      -----------------------------------------
+      -- Has_Single_Return_In_GNATprove_Mode --
+      -----------------------------------------
+
+      function Has_Single_Return_In_GNATprove_Mode return Boolean is
+         Last_Statement : Node_Id := Empty;
+
+         function Check_Return (N : Node_Id) return Traverse_Result;
+         --  Returns OK on node N if this is not a return statement different
+         --  from the last statement in the subprogram.
+
+         ------------------
+         -- Check_Return --
+         ------------------
+
+         function Check_Return (N : Node_Id) return Traverse_Result is
+         begin
+            if Nkind_In (N, N_Simple_Return_Statement,
+                            N_Extended_Return_Statement)
+            then
+               if N = Last_Statement then
+                  return OK;
+               else
+                  return Abandon;
+               end if;
+
+            else
+               return OK;
+            end if;
+         end Check_Return;
+
+         function Check_All_Returns is new Traverse_Func (Check_Return);
+
+      --  Start of processing for Has_Single_Return_In_GNATprove_Mode
+
+      begin
+         --  Retrieve last statement inside possible block statements
+
+         Last_Statement := Last (Statements (Handled_Statement_Sequence (N)));
+
+         while Nkind (Last_Statement) = N_Block_Statement loop
+            Last_Statement :=
+              Last (Statements (Handled_Statement_Sequence (Last_Statement)));
+         end loop;
+
+         --  Check that the last statement is the only possible return
+         --  statement in the subprogram.
+
+         return Check_All_Returns (N) = OK;
+      end Has_Single_Return_In_GNATprove_Mode;
+
       --------------------
       -- Remove_Pragmas --
       --------------------
@@ -1211,6 +1267,16 @@ package body Inline is
       then
          return;
 
+      --  Subprograms that have return statements in the middle of the body are
+      --  inlined with gotos. GNATprove does not currently support gotos, so
+      --  we prevent such inlining.
+
+      elsif GNATprove_Mode
+        and then not Has_Single_Return_In_GNATprove_Mode
+      then
+         Cannot_Inline ("cannot inline & (multiple returns)?", N, Subp);
+         return;
+
       --  Functions that return unconstrained composite types require
       --  secondary stack handling, and cannot currently be inlined, unless
       --  all return statements return a local variable that is the first
@@ -1378,6 +1444,14 @@ package body Inline is
          then
             null;
 
+         --  In GNATprove mode, issue a warning, and indicate that the
+         --  subprogram is not always inlined by setting flag Is_Inlined
+         --  to False.
+
+         elsif GNATprove_Mode then
+            Set_Is_Inlined (Subp, False);
+            Error_Msg_NE (Msg & "p?", N, Subp);
+
          elsif Has_Pragma_Inline_Always (Subp) then
 
             --  Remove last character (question mark) to make this into an
@@ -1399,12 +1473,16 @@ package body Inline is
 
          Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
 
-      --  Do not issue errors/warnings when compiling with optimizations. Note
-      --  that GNATprove mode is only set when we are analyzing (not compiling)
-      --  the program, so in that case the value of optimization level does not
-      --  matter.
+      --  In GNATprove mode, issue a warning, and indicate that the subprogram
+      --  is not always inlined by setting flag Is_Inlined to False.
+
+      elsif GNATprove_Mode then
+         Set_Is_Inlined (Subp, False);
+         Error_Msg_NE (Msg & "p?", N, Subp);
+
+      --  Do not issue errors/warnings when compiling with optimizations
 
-      elsif Optimization_Level = 0 or else GNATprove_Mode then
+      elsif Optimization_Level = 0 then
 
          --  Do not emit warning if this is a predefined unit which is not
          --  the main unit. This behavior is currently provided for backward
@@ -1441,7 +1519,7 @@ package body Inline is
 
             Error_Msg_NE (Msg (Msg'First .. Msg'Last - 1), N, Subp);
 
-         else pragma Assert (Front_End_Inlining or GNATprove_Mode);
+         else pragma Assert (Front_End_Inlining);
             Set_Is_Inlined (Subp, False);
 
             --  When inlining cannot take place we must issue an error.
diff --git a/gcc/ada/makeutl.adb b/gcc/ada/makeutl.adb
index 3b72ed7..7f7d060 100644
--- a/gcc/ada/makeutl.adb
+++ b/gcc/ada/makeutl.adb
@@ -2811,7 +2811,6 @@ package body Makeutl is
          With_Roots : Boolean := False)
       is
          Discard : Boolean;
-         pragma Unreferenced (Discard);
       begin
          Discard := Insert (Source, With_Roots);
       end Insert;
diff --git a/gcc/ada/s-fileio.adb b/gcc/ada/s-fileio.adb
index 8a9c9c1..72f7db8 100644
--- a/gcc/ada/s-fileio.adb
+++ b/gcc/ada/s-fileio.adb
@@ -400,7 +400,6 @@ package body System.File_IO is
       Fptr2   : AFCB_Ptr;
 
       Discard : int;
-      pragma Unreferenced (Discard);
 
    begin
       --  Take a lock to protect global Open_Files data structure
diff --git a/gcc/ada/s-interr-hwint.adb b/gcc/ada/s-interr-hwint.adb
index 9da97cf..8e2950f 100644
--- a/gcc/ada/s-interr-hwint.adb
+++ b/gcc/ada/s-interr-hwint.adb
@@ -31,7 +31,7 @@
 
 --  Invariants:
 
---  All user-handleable signals are masked at all times in all tasks/threads
+--  All user-handlable signals are masked at all times in all tasks/threads
 --  except possibly for the Interrupt_Manager task.
 
 --  When a user task wants to have the effect of masking/unmasking an signal,
@@ -123,8 +123,11 @@ package body System.Interrupts is
    end Interrupt_Manager;
 
    task type Interrupt_Server_Task
-     (Interrupt : Interrupt_ID; Int_Sema : Binary_Semaphore_Id) is
+     (Interrupt : Interrupt_ID;
+      Int_Sema  : Binary_Semaphore_Id)
+   is
       --  Server task for vectored hardware interrupt handling
+
       pragma Interrupt_Priority (System.Interrupt_Priority'First + 2);
    end Interrupt_Server_Task;
 
@@ -152,7 +155,7 @@ package body System.Interrupts is
    --  is specified through the pragma Attach_Handler.
 
    User_Entry : array (Interrupt_ID) of Entry_Assoc :=
-     (others => (T => Null_Task, E => Null_Task_Entry));
+                  (others => (T => Null_Task, E => Null_Task_Entry));
    pragma Volatile_Components (User_Entry);
    --  Holds the task and entry index (if any) for each interrupt / signal
 
@@ -172,19 +175,18 @@ package body System.Interrupts is
    Registered_Handler_Tail : R_Link := null;
 
    Server_ID : array (Interrupt_ID) of System.Tasking.Task_Id :=
-     (others => System.Tasking.Null_Task);
+                 (others => System.Tasking.Null_Task);
    pragma Atomic_Components (Server_ID);
    --  Holds the Task_Id of the Server_Task for each interrupt / signal.
    --  Task_Id is needed to accomplish locking per interrupt base. Also
    --  is needed to determine whether to create a new Server_Task.
 
    Semaphore_ID_Map : array
-     (Interrupt_ID range 0 .. System.OS_Interface.Max_HW_Interrupt)
-      of Binary_Semaphore_Id := (others => 0);
+     (Interrupt_ID range 0 .. System.OS_Interface.Max_HW_Interrupt) of
+        Binary_Semaphore_Id := (others => 0);
    --  Array of binary semaphores associated with vectored interrupts. Note
    --  that the last bound should be Max_HW_Interrupt, but this will raise
-   --  Storage_Error if Num_HW_Interrupts is null, so use an extra 4 bytes
-   --  instead.
+   --  Storage_Error if Num_HW_Interrupts is null so use extra 4 bytes instead.
 
    Interrupt_Access_Hold : Interrupt_Task_Access;
    --  Variable for allocating an Interrupt_Server_Task
@@ -1040,7 +1042,6 @@ package body System.Interrupts is
 
    task body Interrupt_Server_Task is
       Ignore : constant Boolean := System.Tasking.Utilities.Make_Independent;
-      pragma Unreferenced (Ignore);
 
       Self_Id         : constant Task_Id := Self;
       Tmp_Handler     : Parameterless_Handler;
@@ -1052,8 +1053,8 @@ package body System.Interrupts is
       Semaphore_ID_Map (Interrupt) := Int_Sema;
 
       loop
-         --  Pend on semaphore that will be triggered by the
-         --  umbrella handler when the associated interrupt comes in
+         --  Pend on semaphore that will be triggered by the umbrella handler
+         --  when the associated interrupt comes in.
 
          Status := Binary_Semaphore_Obtain (Int_Sema);
          pragma Assert (Status = 0);
@@ -1075,8 +1076,8 @@ package body System.Interrupts is
               (Tmp_ID, Tmp_Entry_Index, System.Null_Address);
 
          else
-            --  Semaphore has been flushed by an unbind operation in
-            --  the Interrupt_Manager. Terminate the server task.
+            --  Semaphore has been flushed by an unbind operation in the
+            --  Interrupt_Manager. Terminate the server task.
 
             --  Wait for the Interrupt_Manager to complete its work
 
diff --git a/gcc/ada/s-interr-sigaction.adb b/gcc/ada/s-interr-sigaction.adb
index f9612d5..2e646a2 100644
--- a/gcc/ada/s-interr-sigaction.adb
+++ b/gcc/ada/s-interr-sigaction.adb
@@ -617,7 +617,6 @@ package body System.Interrupts is
 
    task body Server_Task is
       Ignore : constant Boolean := Utilities.Make_Independent;
-      pragma Unreferenced (Ignore);
 
       Desc    : Handler_Desc renames Descriptors (Interrupt);
       Self_Id : constant Task_Id := STPO.Self;
diff --git a/gcc/ada/s-interr-vms.adb b/gcc/ada/s-interr-vms.adb
index ae3a5c1..1fc141f 100644
--- a/gcc/ada/s-interr-vms.adb
+++ b/gcc/ada/s-interr-vms.adb
@@ -570,7 +570,6 @@ package body System.Interrupts is
       --  away, the Interrupt_Manager will terminate gracefully.
 
       Ignore : constant Boolean := System.Tasking.Utilities.Make_Independent;
-      pragma Unreferenced (Ignore);
 
       --------------------
       -- Local Routines --
@@ -897,7 +896,6 @@ package body System.Interrupts is
       --  goes away, the Server_Task will terminate gracefully.
 
       Ignore : constant Boolean := System.Tasking.Utilities.Make_Independent;
-      pragma Unreferenced (Ignore);
 
       Self_ID         : constant Task_Id := Self;
       Tmp_Handler     : Parameterless_Handler;
@@ -1010,10 +1008,10 @@ package body System.Interrupts is
             POP.Unlock_RTS;
          end if;
 
-         System.Tasking.Initialization.Undefer_Abort (Self_ID);
+         --  Undefer abort here to allow a window for this task to be aborted
+         --  at the time of system shutdown.
 
-         --  Undefer abort here to allow a window for this task
-         --  to be aborted  at the time of system shutdown.
+         System.Tasking.Initialization.Undefer_Abort (Self_ID);
       end loop;
    end Server_Task;
 
diff --git a/gcc/ada/s-interr.adb b/gcc/ada/s-interr.adb
index a9b1208..3c988af 100644
--- a/gcc/ada/s-interr.adb
+++ b/gcc/ada/s-interr.adb
@@ -685,7 +685,6 @@ package body System.Interrupts is
       --  goes away, the Interrupt_Manager will terminate gracefully.
 
       Ignore : constant Boolean := System.Tasking.Utilities.Make_Independent;
-      pragma Unreferenced (Ignore);
 
       ---------------------
       -- Local Variables --
@@ -1241,7 +1240,6 @@ package body System.Interrupts is
       --  away, the Server_Task will terminate gracefully.
 
       Ignore : constant Boolean := System.Tasking.Utilities.Make_Independent;
-      pragma Unreferenced (Ignore);
 
       Intwait_Mask    : aliased IMNG.Interrupt_Mask;
       Ret_Interrupt   : Interrupt_ID;
@@ -1307,7 +1305,7 @@ package body System.Interrupts is
 
          elsif Blocked (Interrupt) then
 
-            --  Interrupt is blocked. Stay here, so we won't catch it
+            --  Interrupt is blocked, stay here, so we won't catch it
 
             Self_ID.Common.State := Interrupt_Server_Blocked_Interrupt_Sleep;
             POP.Sleep (Self_ID, Interrupt_Server_Blocked_Interrupt_Sleep);
diff --git a/gcc/ada/s-os_lib.adb b/gcc/ada/s-os_lib.adb
index 794d30665..940bf51 100644
--- a/gcc/ada/s-os_lib.adb
+++ b/gcc/ada/s-os_lib.adb
@@ -279,7 +279,6 @@ package body System.OS_Lib is
    procedure Close (FD : File_Descriptor) is
       use CRTL;
       Discard : constant int := close (int (FD));
-      pragma Unreferenced (Discard);
    begin
       null;
    end Close;
diff --git a/gcc/ada/s-taasde.adb b/gcc/ada/s-taasde.adb
index 40e3dc6..061ef0d 100644
--- a/gcc/ada/s-taasde.adb
+++ b/gcc/ada/s-taasde.adb
@@ -283,7 +283,6 @@ package body System.Tasking.Async_Delays is
 
    task body Timer_Server is
       Ignore : constant Boolean := STU.Make_Independent;
-      pragma Unreferenced (Ignore);
 
       --  Local Declarations
 
diff --git a/gcc/ada/s-taprop-mingw.adb b/gcc/ada/s-taprop-mingw.adb
index 75d81cb..126ef64 100644
--- a/gcc/ada/s-taprop-mingw.adb
+++ b/gcc/ada/s-taprop-mingw.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                  B o d y                                 --
 --                                                                          --
---          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, 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- --
@@ -1029,7 +1029,6 @@ package body System.Task_Primitives.Operations is
 
    procedure Initialize (Environment_Task : Task_Id) is
       Discard : BOOL;
-      pragma Unreferenced (Discard);
 
    begin
       Environment_Task_Id := Environment_Task;
diff --git a/gcc/ada/s-tasdeb-vms.adb b/gcc/ada/s-tasdeb-vms.adb
index 6c9ae75..0ef6322 100644
--- a/gcc/ada/s-tasdeb-vms.adb
+++ b/gcc/ada/s-tasdeb-vms.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                  B o d y                                 --
 --                                                                          --
---          Copyright (C) 2008-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 2008-2014, 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- --
@@ -2148,11 +2148,12 @@ package body System.Tasking.Debug is
 
    procedure Write (Fd : Integer; S : String; Count : Integer) is
       Discard : System.CRTL.ssize_t;
-      pragma Unreferenced (Discard);
+      --  Ignore write errors here; this is just debugging output, and there's
+      --  nothing to be done about errors anyway.
    begin
-      Discard := System.CRTL.write (Fd, S (S'First)'Address,
-                                    System.CRTL.size_t (Count));
-      --  Is it really right to ignore write errors here ???
+      Discard :=
+        System.CRTL.write
+          (Fd, S (S'First)'Address, System.CRTL.size_t (Count));
    end Write;
 
 end System.Tasking.Debug;
diff --git a/gcc/ada/s-tasdeb.adb b/gcc/ada/s-tasdeb.adb
index 2c8b638..5c084b5 100644
--- a/gcc/ada/s-tasdeb.adb
+++ b/gcc/ada/s-tasdeb.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                  B o d y                                 --
 --                                                                          --
---          Copyright (C) 1997-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1997-2014, 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- --
@@ -396,12 +396,12 @@ package body System.Tasking.Debug is
 
    procedure Write (Fd : Integer; S : String; Count : Integer) is
       Discard : System.CRTL.ssize_t;
-      pragma Unreferenced (Discard);
-   begin
-      Discard := System.CRTL.write (Fd, S'Address,
-                                    System.CRTL.size_t (Count));
       --  Ignore write errors here; this is just debugging output, and there's
       --  nothing to be done about errors anyway.
+   begin
+      Discard :=
+        System.CRTL.write
+          (Fd, S'Address, System.CRTL.size_t (Count));
    end Write;
 
 end System.Tasking.Debug;
diff --git a/gcc/ada/s-taspri-posix.ads b/gcc/ada/s-taspri-posix.ads
index 65f0690..2fa27fd 100644
--- a/gcc/ada/s-taspri-posix.ads
+++ b/gcc/ada/s-taspri-posix.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---            Copyright (C) 1991-1914, Florida State University             --
+--            Copyright (C) 1991-1994, Florida State University             --
 --                     Copyright (C) 1995-2014, AdaCore                     --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
diff --git a/gcc/ada/s-tassta.adb b/gcc/ada/s-tassta.adb
index fb02a53..f8a8a71 100644
--- a/gcc/ada/s-tassta.adb
+++ b/gcc/ada/s-tassta.adb
@@ -814,7 +814,6 @@ package body System.Tasking.Stages is
 
       Ignore_1 : Boolean;
       Ignore_2 : Boolean;
-      pragma Unreferenced (Ignore_1, Ignore_2);
 
       function State
         (Int : System.Interrupt_Management.Interrupt_ID) return Character;
diff --git a/gcc/ada/s-tasuti.adb b/gcc/ada/s-tasuti.adb
index 8449ee5..e194025 100644
--- a/gcc/ada/s-tasuti.adb
+++ b/gcc/ada/s-tasuti.adb
@@ -322,7 +322,10 @@ package body System.Tasking.Utilities is
 
       Initialization.Undefer_Abort (Self_Id);
 
-      return True; -- return value doesn't matter
+      --  Return True. Actually the return value is junk, since we expect it
+      --  always to be ignored (see spec), but we have to return something!
+
+      return True;
    end Make_Independent;
 
    ------------------
diff --git a/gcc/ada/s-tasuti.ads b/gcc/ada/s-tasuti.ads
index b200371..8754892 100644
--- a/gcc/ada/s-tasuti.ads
+++ b/gcc/ada/s-tasuti.ads
@@ -70,7 +70,6 @@ package System.Tasking.Utilities is
    --     task body Some_Independent_Task is
    --        ...
    --        Ignore : constant Boolean := Make_Independent;
-   --        pragma Unreferenced (Ignore);
    --        ...
    --     begin
    --
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 4d0264f..c18718e 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -3038,6 +3038,7 @@ package body Sem_Ch6 is
                  and then GNATprove_Mode
                  and then Debug_Flag_QQ
                  and then Full_Analysis
+                 and then Nkind (N) /= N_Subprogram_Body_Stub
                  and then Comes_From_Source (Body_Id)
                  and then Is_List_Member (N)
                  and then not Body_Has_Contract
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 68b9748..fee781c 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -15804,9 +15804,7 @@ package body Sem_Prag is
             Type_Id : Node_Id;
             Typ     : Entity_Id;
             PDecl   : Node_Id;
-
             Discard : Boolean;
-            pragma Unreferenced (Discard);
 
          begin
             GNAT_Pragma;
@@ -18201,9 +18199,7 @@ package body Sem_Prag is
          when Pragma_Predicate => Predicate : declare
             Type_Id : Node_Id;
             Typ     : Entity_Id;
-
             Discard : Boolean;
-            pragma Unreferenced (Discard);
 
          begin
             GNAT_Pragma;
diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads
index d9bf0bc..68746d6 100644
--- a/gcc/ada/sem_util.ads
+++ b/gcc/ada/sem_util.ads
@@ -1211,7 +1211,7 @@ package Sem_Util is
    --    junk
    --    unused
    --  Used to suppress warnings on names matching these patterns. The contents
-   --  of Name_Buffer and Name_Len are desteoyed by this call.
+   --  of Name_Buffer and Name_Len are destroyed by this call.
 
    type Is_LHS_Result is (Yes, No, Unknown);
    function Is_LHS (N : Node_Id) return Is_LHS_Result;