[multiple changes]
2014-05-21 Javier Miranda <miranda@adacore.com> * exp_ch4.adb (Expand_Allocator_Expression.Apply_Accessibility_Check): Complete previous patch. 2014-05-21 Thomas Quinot <quinot@adacore.com> * g-socket.adb (Read and Write for Datagram_Socket_Stream_Type): Provide a behaviour more consistent with underlying datagram socket: do not attempt to loop over Send_Socket/Receive_Socket iterating along the buffer. 2014-05-21 Hristian Kirtchev <kirtchev@adacore.com> * freeze.adb (Freeze_Record_Type): Ensure that a discriminated or a tagged type is not labelled as volatile. Ensure that a non-volatile type has no volatile components. * sem_ch3.adb (Analyze_Object_Contract): Add local constant Obj_Typ. Code reformatting. Ensure that a discriminated or tagged object is not labelled as volatile. * sem_prag.adb (Process_Atomic_Shared_Volatile): Ensure that pragma Volatile applies to a full type declaration or an object declaration when SPARK mode is on. 2014-05-21 Sergey Rybin <rybin@adacore.com frybin> * gnat_ugn.texi: For ASIS tools, reword the paragraph about providing options needed for compiling the argument source for the situation when a project file can be used as a tool parameter. 2014-05-21 Gary Dismukes <dismukes@adacore.com> * gnat_rm.texi: Minor typo fix. From-SVN: r210697
This commit is contained in:
parent
da574a866b
commit
601bb6b35e
8 changed files with 205 additions and 131 deletions
|
@ -1,3 +1,37 @@
|
|||
2014-05-21 Javier Miranda <miranda@adacore.com>
|
||||
|
||||
* exp_ch4.adb (Expand_Allocator_Expression.Apply_Accessibility_Check):
|
||||
Complete previous patch.
|
||||
|
||||
2014-05-21 Thomas Quinot <quinot@adacore.com>
|
||||
|
||||
* g-socket.adb (Read and Write for Datagram_Socket_Stream_Type):
|
||||
Provide a behaviour more consistent with underlying datagram
|
||||
socket: do not attempt to loop over Send_Socket/Receive_Socket
|
||||
iterating along the buffer.
|
||||
|
||||
2014-05-21 Hristian Kirtchev <kirtchev@adacore.com>
|
||||
|
||||
* freeze.adb (Freeze_Record_Type): Ensure that a discriminated
|
||||
or a tagged type is not labelled as volatile. Ensure that a
|
||||
non-volatile type has no volatile components.
|
||||
* sem_ch3.adb (Analyze_Object_Contract): Add local constant
|
||||
Obj_Typ. Code reformatting. Ensure that a discriminated or
|
||||
tagged object is not labelled as volatile.
|
||||
* sem_prag.adb (Process_Atomic_Shared_Volatile): Ensure that
|
||||
pragma Volatile applies to a full type declaration or an object
|
||||
declaration when SPARK mode is on.
|
||||
|
||||
2014-05-21 Sergey Rybin <rybin@adacore.com frybin>
|
||||
|
||||
* gnat_ugn.texi: For ASIS tools, reword the paragraph about
|
||||
providing options needed for compiling the argument source for
|
||||
the situation when a project file can be used as a tool parameter.
|
||||
|
||||
2014-05-21 Gary Dismukes <dismukes@adacore.com>
|
||||
|
||||
* gnat_rm.texi: Minor typo fix.
|
||||
|
||||
2014-05-21 Robert Dewar <dewar@adacore.com>
|
||||
|
||||
* stand.adb (Tree_Read): Read missing entities.
|
||||
|
|
|
@ -835,7 +835,8 @@ package body Exp_Ch4 is
|
|||
-- object Obj_Ref already references the tag of the secondary
|
||||
-- dispatch table.
|
||||
|
||||
if Present (Parent (Entity (Obj_Ref)))
|
||||
if Nkind (Obj_Ref) in N_Has_Entity
|
||||
and then Present (Entity (Obj_Ref))
|
||||
and then Present (Renamed_Object (Entity (Obj_Ref)))
|
||||
and then Is_Interface (DesigT)
|
||||
then
|
||||
|
|
|
@ -3314,6 +3314,45 @@ package body Freeze is
|
|||
end if;
|
||||
end if;
|
||||
|
||||
-- The following checks are only relevant when SPARK_Mode is on as
|
||||
-- they are not standard Ada legality rules.
|
||||
|
||||
if SPARK_Mode = On then
|
||||
if Is_SPARK_Volatile_Object (Rec) then
|
||||
|
||||
-- A discriminated type cannot be volatile (SPARK RM C.6(4))
|
||||
|
||||
if Has_Discriminants (Rec) then
|
||||
Error_Msg_N ("discriminated type & cannot be volatile", Rec);
|
||||
|
||||
-- A tagged type cannot be volatile (SPARK RM C.6(5))
|
||||
|
||||
elsif Is_Tagged_Type (Rec) then
|
||||
Error_Msg_N ("tagged type & cannot be volatile", Rec);
|
||||
end if;
|
||||
|
||||
-- A non-volatile record type cannot contain volatile components
|
||||
-- (SPARK RM C.6(2)). The check is performed at freeze point
|
||||
-- because the volatility status of the record type and its
|
||||
-- components is clearly known.
|
||||
|
||||
else
|
||||
Comp := First_Component (Rec);
|
||||
while Present (Comp) loop
|
||||
if Comes_From_Source (Comp)
|
||||
and then Is_SPARK_Volatile_Object (Comp)
|
||||
then
|
||||
Error_Msg_Name_1 := Chars (Rec);
|
||||
Error_Msg_N
|
||||
("component & of non-volatile record type % cannot be "
|
||||
& "volatile", Comp);
|
||||
end if;
|
||||
|
||||
Next_Component (Comp);
|
||||
end loop;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
-- All done if not a full record definition
|
||||
|
||||
if Ekind (Rec) /= E_Record_Type then
|
||||
|
|
|
@ -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- --
|
||||
|
@ -244,13 +244,6 @@ package body GNAT.Sockets is
|
|||
(Stream : in out Stream_Socket_Stream_Type;
|
||||
Item : Ada.Streams.Stream_Element_Array);
|
||||
|
||||
procedure Stream_Write
|
||||
(Socket : Socket_Type;
|
||||
Item : Ada.Streams.Stream_Element_Array;
|
||||
To : access Sock_Addr_Type);
|
||||
-- Common implementation for the Write operation of Datagram_Socket_Stream_
|
||||
-- Type and Stream_Socket_Stream_Type.
|
||||
|
||||
procedure Wait_On_Socket
|
||||
(Socket : Socket_Type;
|
||||
For_Read : Boolean;
|
||||
|
@ -1732,27 +1725,12 @@ package body GNAT.Sockets is
|
|||
Item : out Ada.Streams.Stream_Element_Array;
|
||||
Last : out Ada.Streams.Stream_Element_Offset)
|
||||
is
|
||||
First : Ada.Streams.Stream_Element_Offset := Item'First;
|
||||
Index : Ada.Streams.Stream_Element_Offset := First - 1;
|
||||
Max : constant Ada.Streams.Stream_Element_Offset := Item'Last;
|
||||
|
||||
begin
|
||||
loop
|
||||
Receive_Socket
|
||||
(Stream.Socket,
|
||||
Item (First .. Max),
|
||||
Index,
|
||||
Stream.From);
|
||||
|
||||
Last := Index;
|
||||
|
||||
-- Exit when all or zero data received. Zero means that the socket
|
||||
-- peer is closed.
|
||||
|
||||
exit when Index < First or else Index = Max;
|
||||
|
||||
First := Index + 1;
|
||||
end loop;
|
||||
Receive_Socket
|
||||
(Stream.Socket,
|
||||
Item,
|
||||
Last,
|
||||
Stream.From);
|
||||
end Read;
|
||||
|
||||
----------
|
||||
|
@ -2419,43 +2397,6 @@ package body GNAT.Sockets is
|
|||
return Stream_Access (S);
|
||||
end Stream;
|
||||
|
||||
------------------
|
||||
-- Stream_Write --
|
||||
------------------
|
||||
|
||||
procedure Stream_Write
|
||||
(Socket : Socket_Type;
|
||||
Item : Ada.Streams.Stream_Element_Array;
|
||||
To : access Sock_Addr_Type)
|
||||
is
|
||||
First : Ada.Streams.Stream_Element_Offset;
|
||||
Index : Ada.Streams.Stream_Element_Offset;
|
||||
Max : constant Ada.Streams.Stream_Element_Offset := Item'Last;
|
||||
|
||||
begin
|
||||
First := Item'First;
|
||||
Index := First - 1;
|
||||
while First <= Max loop
|
||||
Send_Socket (Socket, Item (First .. Max), Index, To);
|
||||
|
||||
-- Exit when all or zero data sent. Zero means that the socket has
|
||||
-- been closed by peer.
|
||||
|
||||
exit when Index < First or else Index = Max;
|
||||
|
||||
First := Index + 1;
|
||||
end loop;
|
||||
|
||||
-- For an empty array, we have First > Max, and hence Index >= Max (no
|
||||
-- error, the loop above is never executed). After a successful send,
|
||||
-- Index = Max. The only remaining case, Index < Max, is therefore
|
||||
-- always an actual send failure.
|
||||
|
||||
if Index < Max then
|
||||
Raise_Socket_Error (Socket_Errno);
|
||||
end if;
|
||||
end Stream_Write;
|
||||
|
||||
----------
|
||||
-- To_C --
|
||||
----------
|
||||
|
@ -2695,8 +2636,20 @@ package body GNAT.Sockets is
|
|||
(Stream : in out Datagram_Socket_Stream_Type;
|
||||
Item : Ada.Streams.Stream_Element_Array)
|
||||
is
|
||||
Last : Stream_Element_Offset;
|
||||
|
||||
begin
|
||||
Stream_Write (Stream.Socket, Item, To => Stream.To'Unrestricted_Access);
|
||||
Send_Socket
|
||||
(Stream.Socket,
|
||||
Item,
|
||||
Last,
|
||||
Stream.To);
|
||||
|
||||
-- It is an error if not all of the data has been sent
|
||||
|
||||
if Last /= Item'Last then
|
||||
Raise_Socket_Error (Socket_Errno);
|
||||
end if;
|
||||
end Write;
|
||||
|
||||
-----------
|
||||
|
@ -2707,8 +2660,32 @@ package body GNAT.Sockets is
|
|||
(Stream : in out Stream_Socket_Stream_Type;
|
||||
Item : Ada.Streams.Stream_Element_Array)
|
||||
is
|
||||
First : Ada.Streams.Stream_Element_Offset;
|
||||
Index : Ada.Streams.Stream_Element_Offset;
|
||||
Max : constant Ada.Streams.Stream_Element_Offset := Item'Last;
|
||||
|
||||
begin
|
||||
Stream_Write (Stream.Socket, Item, To => null);
|
||||
First := Item'First;
|
||||
Index := First - 1;
|
||||
while First <= Max loop
|
||||
Send_Socket (Stream.Socket, Item (First .. Max), Index, null);
|
||||
|
||||
-- Exit when all or zero data sent. Zero means that the socket has
|
||||
-- been closed by peer.
|
||||
|
||||
exit when Index < First or else Index = Max;
|
||||
|
||||
First := Index + 1;
|
||||
end loop;
|
||||
|
||||
-- For an empty array, we have First > Max, and hence Index >= Max (no
|
||||
-- error, the loop above is never executed). After a successful send,
|
||||
-- Index = Max. The only remaining case, Index < Max, is therefore
|
||||
-- always an actual send failure.
|
||||
|
||||
if Index < Max then
|
||||
Raise_Socket_Error (Socket_Errno);
|
||||
end if;
|
||||
end Write;
|
||||
|
||||
Sockets_Library_Controller_Object : Sockets_Library_Controller;
|
||||
|
|
|
@ -15746,7 +15746,7 @@ end Overwrite_Array;
|
|||
@end smallexample
|
||||
|
||||
@noindent
|
||||
then the program compiles without the waraning and when run will generate
|
||||
then the program compiles without the warning and when run will generate
|
||||
the output @code{X was not clobbered}.
|
||||
|
||||
@node Effect of Convention on Representation
|
||||
|
|
|
@ -14129,22 +14129,18 @@ Support for @option{--pp-old} will be removed in some future version.
|
|||
|
||||
To produce a reformatted file, @command{gnatpp} invokes the Ada
|
||||
compiler and generates and uses the ASIS tree for the input source;
|
||||
thus the input must be legal Ada code.
|
||||
thus the input must be legal Ada code, and the tool should have all the
|
||||
information needed to compile the input source. To provide this information,
|
||||
you may specify as a tool parameter the project file the input source belongs to
|
||||
(or you may call @command{gnatpp}
|
||||
through the @command{gnat} driver (see @ref{The GNAT Driver and
|
||||
Project Files}). Another possibility is to specify the source search
|
||||
path and needed configuration files in @option{-cargs} section of @command{gnatpp}
|
||||
call, see the description of the @command{gnatpp} switches below.
|
||||
|
||||
@command{gnatpp} cannot process sources that contain
|
||||
preprocessing directives.
|
||||
|
||||
If the compilation unit contained in the input source depends
|
||||
semantically upon units located outside the current directory, you
|
||||
have to provide the source search path when invoking
|
||||
@command{gnatpp}. If these units are contained in files with names
|
||||
that do not follow the GNAT file naming rules, you have to provide a
|
||||
configuration file describing the corresponding naming scheme; see the
|
||||
description of the @command{gnatpp} switches below. Another
|
||||
possibility is to use a project file and to call @command{gnatpp}
|
||||
through the @command{gnat} driver (see @ref{The GNAT Driver and
|
||||
Project Files}).
|
||||
|
||||
The @command{gnatpp} command has the form
|
||||
|
||||
@smallexample
|
||||
|
@ -15579,23 +15575,16 @@ metrics are computed and output.
|
|||
* Switches for gnatmetric::
|
||||
@end menu
|
||||
|
||||
@command{gnatmetric} generates and uses the ASIS
|
||||
tree for the input source and thus requires the input to be syntactically and
|
||||
semantically legal.
|
||||
If this condition is not met, @command{gnatmetric} will generate
|
||||
an error message; no metric information for this file will be
|
||||
computed and reported.
|
||||
|
||||
If the compilation unit contained in the input source depends semantically
|
||||
upon units in files located outside the current directory, you have to provide
|
||||
the source search path when invoking @command{gnatmetric}.
|
||||
If it depends semantically upon units that are contained
|
||||
in files with names that do not follow the GNAT file naming rules, you have to
|
||||
provide the configuration file describing the corresponding naming scheme (see
|
||||
the description of the @command{gnatmetric} switches below.)
|
||||
Alternatively, you may use a project file and invoke @command{gnatmetric}
|
||||
through the @command{gnat} driver (see @ref{The GNAT Driver and Project Files}),
|
||||
or you can directly specify a project file as a @command{gnatmetric} parameter.
|
||||
To compute program metrics, @command{gnatmetric} invokes the Ada
|
||||
compiler and generates and uses the ASIS tree for the input source;
|
||||
thus the input must be legal Ada code, and the tool should have all the
|
||||
information needed to compile the input source. To provide this information,
|
||||
you may specify as a tool parameter the project file the input source belongs to
|
||||
(or you may call @command{gnatmetric}
|
||||
through the @command{gnat} driver (see @ref{The GNAT Driver and
|
||||
Project Files}). Another possibility is to specify the source search
|
||||
path and needed configuration files in @option{-cargs} section of @command{gnatmetric}
|
||||
call, see the description of the @command{gnatmetric} switches below.
|
||||
|
||||
The @command{gnatmetric} command has the form
|
||||
|
||||
|
@ -16427,8 +16416,8 @@ dependencies between units that are arguments of the @command{gnatmetric}
|
|||
invocation. Coupling metrics are program-wide (or project-wide) metrics, so
|
||||
you should invoke @command{gnatmetric} for
|
||||
the complete set of sources comprising your program. This can be done
|
||||
by invoking @command{gnatmetric} from the GNAT driver with the @option{-U}
|
||||
option (see @ref{The GNAT Driver and Project Files} for details).
|
||||
by invoking @command{gnatmetric} with the corresponding project file
|
||||
and with the @option{-U} option.
|
||||
|
||||
By default, all the coupling metrics are disabled. You can use the following
|
||||
switches to specify the coupling metrics to be computed and reported:
|
||||
|
@ -19315,15 +19304,16 @@ For full details, refer to @cite{GNATcheck Reference Manual} document.
|
|||
@command{gnatstub} creates body stubs, that is, empty but compilable bodies
|
||||
for library unit declarations.
|
||||
|
||||
Note: to invoke @code{gnatstub} with a project file, use the @code{gnat}
|
||||
driver (see @ref{The GNAT Driver and Project Files}).
|
||||
|
||||
To create a body stub, @command{gnatstub} has to compile the library
|
||||
unit declaration. Therefore, bodies can be created only for legal
|
||||
library units. Moreover, if a library unit depends semantically upon
|
||||
units located outside the current directory, you have to provide
|
||||
the source search path when calling @command{gnatstub}, see the description
|
||||
of @command{gnatstub} switches below.
|
||||
To create a body stub, @command{gnatstub} invokes the Ada
|
||||
compiler and generates and uses the ASIS tree for the input source;
|
||||
thus the input must be legal Ada code, and the tool should have all the
|
||||
information needed to compile the input source. To provide this information,
|
||||
you may specify as a tool parameter the project file the input source belongs to
|
||||
(or you may call @command{gnatstub}
|
||||
through the @command{gnat} driver (see @ref{The GNAT Driver and
|
||||
Project Files}). Another possibility is to specify the source search
|
||||
path and needed configuration files in @option{-cargs} section of @command{gnatstub}
|
||||
call, see the description of the @command{gnatstub} switches below.
|
||||
|
||||
By default, all the program unit body stubs generated by @code{gnatstub}
|
||||
raise the predefined @code{Program_Error} exception, which will catch
|
||||
|
|
|
@ -2980,12 +2980,13 @@ package body Sem_Ch3 is
|
|||
-----------------------------
|
||||
|
||||
procedure Analyze_Object_Contract (Obj_Id : Entity_Id) is
|
||||
AR_Val : Boolean := False;
|
||||
AW_Val : Boolean := False;
|
||||
ER_Val : Boolean := False;
|
||||
EW_Val : Boolean := False;
|
||||
Prag : Node_Id;
|
||||
Seen : Boolean := False;
|
||||
Obj_Typ : constant Entity_Id := Etype (Obj_Id);
|
||||
AR_Val : Boolean := False;
|
||||
AW_Val : Boolean := False;
|
||||
ER_Val : Boolean := False;
|
||||
EW_Val : Boolean := False;
|
||||
Prag : Node_Id;
|
||||
Seen : Boolean := False;
|
||||
|
||||
begin
|
||||
if Ekind (Obj_Id) = E_Constant then
|
||||
|
@ -3008,26 +3009,43 @@ package body Sem_Ch3 is
|
|||
-- they are not standard Ada legality rules.
|
||||
|
||||
if SPARK_Mode = On then
|
||||
if Is_SPARK_Volatile_Object (Obj_Id) then
|
||||
|
||||
-- A non-volatile object cannot have volatile components
|
||||
-- (SPARK RM 7.1.3(7)).
|
||||
-- The declaration of a volatile object must appear at the
|
||||
-- library level (SPARK RM 7.1.3(7), C.6(6)).
|
||||
|
||||
if not Is_SPARK_Volatile_Object (Obj_Id)
|
||||
and then Has_Volatile_Component (Etype (Obj_Id))
|
||||
then
|
||||
Error_Msg_N
|
||||
("non-volatile variable & cannot have volatile components",
|
||||
Obj_Id);
|
||||
if not Is_Library_Level_Entity (Obj_Id) then
|
||||
Error_Msg_N
|
||||
("volatile variable & must be declared at library level",
|
||||
Obj_Id);
|
||||
|
||||
-- The declaration of a volatile object must appear at the library
|
||||
-- level.
|
||||
-- An object of a discriminated type cannot be volatile
|
||||
-- (SPARK RM C.6(4)).
|
||||
|
||||
elsif Is_SPARK_Volatile_Object (Obj_Id)
|
||||
and then not Is_Library_Level_Entity (Obj_Id)
|
||||
then
|
||||
Error_Msg_N
|
||||
("volatile variable & must be declared at library level "
|
||||
& "(SPARK RM 7.1.3(5))", Obj_Id);
|
||||
elsif Has_Discriminants (Obj_Typ) then
|
||||
Error_Msg_N
|
||||
("discriminated object & cannot be volatile", Obj_Id);
|
||||
|
||||
-- An object of a tagged type cannot be volatile
|
||||
-- (SPARK RM C.6(5)).
|
||||
|
||||
elsif Is_Tagged_Type (Obj_Typ) then
|
||||
Error_Msg_N ("tagged object & cannot be volatile", Obj_Id);
|
||||
end if;
|
||||
|
||||
-- The object is not volatile
|
||||
|
||||
else
|
||||
-- A non-volatile object cannot have volatile components
|
||||
-- (SPARK RM 7.1.3(7)).
|
||||
|
||||
if not Is_SPARK_Volatile_Object (Obj_Id)
|
||||
and then Has_Volatile_Component (Obj_Typ)
|
||||
then
|
||||
Error_Msg_N
|
||||
("non-volatile object & cannot have volatile components",
|
||||
Obj_Id);
|
||||
end if;
|
||||
end if;
|
||||
end if;
|
||||
|
||||
|
|
|
@ -6387,6 +6387,21 @@ package body Sem_Prag is
|
|||
Error_Pragma_Arg
|
||||
("inappropriate entity for pragma%", Arg1);
|
||||
end if;
|
||||
|
||||
-- The following check are only relevant when SPARK_Mode is on as
|
||||
-- those are not a standard Ada legality rule. Pragma Volatile can
|
||||
-- only apply to a full type declaration or an object declaration
|
||||
-- (SPARK RM C.6(1)).
|
||||
|
||||
if SPARK_Mode = On
|
||||
and then Prag_Id = Pragma_Volatile
|
||||
and then not Nkind_In (K, N_Full_Type_Declaration,
|
||||
N_Object_Declaration)
|
||||
then
|
||||
Error_Pragma_Arg
|
||||
("argument of pragma % must denote a full type or object "
|
||||
& "declaration", Arg1);
|
||||
end if;
|
||||
end Process_Atomic_Shared_Volatile;
|
||||
|
||||
-------------------------------------------
|
||||
|
|
Loading…
Add table
Reference in a new issue