OpenE2K
/
gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Annotate standard File_Type with Default_Initial_Condition (for SPARK) 

GNATprove was emitting spurious checks about objects of the File_Type being
uninitialized and there was no easy to fix that (those checks could only be
silenced by pragma Annotate or by hiding File_Type behind as SPARK wrapper).

Now the full view of File_Type is annotated with Default_Initial_Condition
and GNATprove knows that objects of that type are default-initialized. The
default initialization is implicitly defined in the Ada RM (as indeed
there is no procedure that would take an IN OUT parameter of that type).

Semantics of Ada programs shall not be affected by these annotations,
so no frontend test is provided. It only affects GNATprove.

2018-01-11  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* libgnat/a-direio.ads, libgnat/a-sequio.ads, libgnat/a-ststio.ads,
	libgnat/a-textio.ads, libgnat/a-witeio.ads, libgnat/a-ztexio.ads
	(File_Type): Add Default_Initial_Condition aspect.

From-SVN: r256502
This commit is contained in:
Piotr Trojanek 2018-01-11 08:52:43 +00:00 committed by Pierre-Marie de Rodat
parent 7d1553e2b6
commit 210fef2d1c
7 changed files with 12 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
gcc/ada/ChangeLog
View File

@ -1,3 +1,9 @@
2018-01-11 Piotr Trojanek <trojanek@adacore.com>
* libgnat/a-direio.ads, libgnat/a-sequio.ads, libgnat/a-ststio.ads,
libgnat/a-textio.ads, libgnat/a-witeio.ads, libgnat/a-ztexio.ads
(File_Type): Add Default_Initial_Condition aspect.
2018-01-11 Pascal Obry <obry@adacore.com>
* libgnat/s-os_lib.adb (Normalize_Pathname): New implementation.

2
gcc/ada/libgnat/a-direio.ads
View File

@ -50,7 +50,7 @@ package Ada.Direct_IO is
(Element_Type'Has_Tagged_Values,
"Element_Type for Direct_IO instance has tagged values");
type File_Type is limited private;
type File_Type is limited private with Default_Initial_Condition;
type File_Mode is (In_File, Inout_File, Out_File);

2
gcc/ada/libgnat/a-sequio.ads
View File

@ -50,7 +50,7 @@ package Ada.Sequential_IO is
(Element_Type'Has_Tagged_Values,
"Element_Type for Sequential_IO instance has tagged values");
type File_Type is limited private;
type File_Type is limited private with Default_Initial_Condition;
type File_Mode is (In_File, Out_File, Append_File);

2
gcc/ada/libgnat/a-ststio.ads
View File

@ -41,7 +41,7 @@ package Ada.Streams.Stream_IO is
type Stream_Access is access all Root_Stream_Type'Class;
type File_Type is limited private;
type File_Type is limited private with Default_Initial_Condition;
type File_Mode is (In_File, Out_File, Append_File);

2
gcc/ada/libgnat/a-textio.ads
View File

@ -49,7 +49,7 @@ with System.WCh_Con;
package Ada.Text_IO is
pragma Elaborate_Body;
type File_Type is limited private;
type File_Type is limited private with Default_Initial_Condition;
type File_Mode is (In_File, Out_File, Append_File);
-- The following representation clause allows the use of unchecked

2
gcc/ada/libgnat/a-witeio.ads
View File

@ -51,7 +51,7 @@ with System.WCh_Con;
package Ada.Wide_Text_IO is
type File_Type is limited private;
type File_Type is limited private with Default_Initial_Condition;
type File_Mode is (In_File, Out_File, Append_File);
-- The following representation clause allows the use of unchecked

2
gcc/ada/libgnat/a-ztexio.ads
View File

@ -51,7 +51,7 @@ with System.WCh_Con;
package Ada.Wide_Wide_Text_IO is
type File_Type is limited private;
type File_Type is limited private with Default_Initial_Condition;
type File_Mode is (In_File, Out_File, Append_File);
-- The following representation clause allows the use of unchecked