From 210fef2d1c7b47c0587375d87d4f4a65f28ca57e Mon Sep 17 00:00:00 2001 From: Piotr Trojanek Date: Thu, 11 Jan 2018 08:52:43 +0000 Subject: [PATCH] [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 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 --- gcc/ada/ChangeLog | 6 ++++++ gcc/ada/libgnat/a-direio.ads | 2 +- gcc/ada/libgnat/a-sequio.ads | 2 +- gcc/ada/libgnat/a-ststio.ads | 2 +- gcc/ada/libgnat/a-textio.ads | 2 +- gcc/ada/libgnat/a-witeio.ads | 2 +- gcc/ada/libgnat/a-ztexio.ads | 2 +- 7 files changed, 12 insertions(+), 6 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index af01944f740..9c104eceabd 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2018-01-11 Piotr Trojanek + + * 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 * 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 96ed11d97fc..fced84c01bd 100644 --- 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 6d2d568c5d0..68773675397 100644 --- 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 efcb5fc6925..7349aea87af 100644 --- 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 5c8589231b1..33ba5fca5a1 100644 --- 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 bbf35eb8563..578149bfa7e 100644 --- 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 730fc026723..efcd5028dd9 100644 --- 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 -- 2.30.2