[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index af01944f74003fed6d7c24899aca6d298835ff39..9c104eceabd6abd996bfcff590e37dcb6fadda87 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -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.

diff --git a/gcc/ada/libgnat/a-direio.ads b/gcc/ada/libgnat/a-direio.ads
index 96ed11d97fc5c643e221383f7e50ef6076ffe81d..fced84c01bddf10bd8dac608636ba40da239539f 100644 (file)
--- a/gcc/ada/libgnat/a-direio.ads
+++ b/gcc/ada/libgnat/a-direio.ads
@@ -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);
 

diff --git a/gcc/ada/libgnat/a-sequio.ads b/gcc/ada/libgnat/a-sequio.ads
index 6d2d568c5d04fb1539b7ac1aea25208bff260d38..6877367539726232ed39de3d2cfbfba25695899b 100644 (file)
--- a/gcc/ada/libgnat/a-sequio.ads
+++ b/gcc/ada/libgnat/a-sequio.ads
@@ -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);
 

diff --git a/gcc/ada/libgnat/a-ststio.ads b/gcc/ada/libgnat/a-ststio.ads
index efcb5fc69255015ae1b04fc527bdfe179e8de198..7349aea87af5e230e819905c07372d324177d6c5 100644 (file)
--- a/gcc/ada/libgnat/a-ststio.ads
+++ b/gcc/ada/libgnat/a-ststio.ads
@@ -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);
 

diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads
index 5c8589231b137ef0c129673adfde25f473e91fbf..33ba5fca5a110b0e2760f6896d045a13f324a1f4 100644 (file)
--- a/gcc/ada/libgnat/a-textio.ads
+++ b/gcc/ada/libgnat/a-textio.ads
@@ -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

diff --git a/gcc/ada/libgnat/a-witeio.ads b/gcc/ada/libgnat/a-witeio.ads
index bbf35eb856340de328f47b4c4504df811c18b946..578149bfa7e42330c0a0500e538b458ef360f155 100644 (file)
--- a/gcc/ada/libgnat/a-witeio.ads
+++ b/gcc/ada/libgnat/a-witeio.ads
@@ -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

diff --git a/gcc/ada/libgnat/a-ztexio.ads b/gcc/ada/libgnat/a-ztexio.ads
index 730fc02672300edba47272dc16a13d3b145e9f1f..efcd5028dd93d00a80611caf138278056d398a4a 100644 (file)
--- a/gcc/ada/libgnat/a-ztexio.ads
+++ b/gcc/ada/libgnat/a-ztexio.ads
@@ -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