[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
This commit is contained in:
Arnaud Charlet 2014-07-30 14:50:43 +02:00
parent b0c5fdda66
commit 7b2888e62c
29 changed files with 156 additions and 67 deletions

View File

@ -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

View File

@ -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.

View File

@ -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;

View File

@ -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;

View File

@ -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);

View File

@ -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;

View File

@ -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

View File

@ -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);

View File

@ -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);

View File

@ -1796,7 +1796,6 @@ begin
declare
Discard : ALI_Id;
pragma Unreferenced (Discard);
begin
Discard :=
Scan_ALI

View File

@ -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 Optimization_Level = 0 or else GNATprove_Mode then
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 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.

View File

@ -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;

View File

@ -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

View File

@ -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

View File

@ -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;

View File

@ -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;

View File

@ -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);

View File

@ -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;

View File

@ -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

View File

@ -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;

View File

@ -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;

View File

@ -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;

View File

@ -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 --

View File

@ -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;

View File

@ -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;
------------------

View File

@ -70,7 +70,6 @@ package System.Tasking.Utilities is
-- task body Some_Independent_Task is
-- ...
-- Ignore : constant Boolean := Make_Independent;
-- pragma Unreferenced (Ignore);
-- ...
-- begin
--

View File

@ -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

View File

@ -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;

View File

@ -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;