Skip to content

R
riscv-gcc-1
Commit 2ff7c604 by Joffrey Huguet Committed by Pierre-Marie de Rodat
Options

[Ada] Add contracts to Ada.Text_IO for SPARK 

This change removes the warnings returned when using Ada.Text_IO library
in SPARK. An abstract state and global contracts were added to modelize
the action of Text_IO procedures and function on the memory and the
files.

2019-07-05  Joffrey Huguet  <huguet@adacore.com>

gcc/ada/

	* libgnat/a-textio.adb: Add abstract state refinment.
	* libgnat/a-textio.ads: Add File_System abstract state.  Add
	global contracts, contract cases, preconditions and
	postconditions to procedures and functions.
	(Set_Input, Set_Output, Set_Error, Standard_Input,
	Standard_Output, Standard_Error, Current_Input, Current_Output,
	Current_Error): Turn SPARK_Mode off.
	(Get_Line): Turn SPARK_Mode off on Get_Line functions.
	* libgnat/a-tideio.ads, libgnat/a-tienio.ads,
	libgnat/a-tifiio.ads, libgnat/a-tiflio.ads,
	libgnat/a-tiinio.ads, libgnat/a-timoio.ads: Add global
	contracts, contract cases, preconditions and postconditions to
	procedures and functions.

From-SVN: r273127
parent b7469acf
Showing with 200 additions and 37 deletions
gcc/ada/ChangeLog
2019-07-05 Joffrey Huguet <huguet@adacore.com>
* libgnat/a-textio.adb: Add abstract state refinment.
* libgnat/a-textio.ads: Add File_System abstract state. Add
global contracts, contract cases, preconditions and
postconditions to procedures and functions.
(Set_Input, Set_Output, Set_Error, Standard_Input,
Standard_Output, Standard_Error, Current_Input, Current_Output,
Current_Error): Turn SPARK_Mode off.
(Get_Line): Turn SPARK_Mode off on Get_Line functions.
* libgnat/a-tideio.ads, libgnat/a-tienio.ads,
libgnat/a-tifiio.ads, libgnat/a-tiflio.ads,
libgnat/a-tiinio.ads, libgnat/a-timoio.ads: Add global
contracts, contract cases, preconditions and postconditions to
procedures and functions.
2019-07-05 Arnaud Charlet <charlet@adacore.com>
* doc/gnat_ugn/platform_specific_information.rst: Refresh doc on
......
gcc/ada/libgnat/a-textio.adb
......@@ -43,7 +43,18 @@ with Ada.Unchecked_Deallocation;
pragma Elaborate_All (System.File_IO);
-- Needed because of calls to Chain_File in package body elaboration
package body Ada.Text_IO is
package body Ada.Text_IO with
Refined_State => (File_System => (Standard_In,
Standard_Out,
Standard_Err,
Current_In,
Current_Out,
Current_Err,
In_Name,
Out_Name,
Err_Name,
WC_Encoding))
is
package FIO renames System.File_IO;
......
gcc/ada/libgnat/a-tideio.ads
......@@ -52,35 +52,58 @@ package Ada.Text_IO.Decimal_IO is
procedure Get
(File : File_Type;
Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (In_Out => File_System);
procedure Get
(Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Put
(File : File_Type;
Item : Num;
Fore : Field := Default_Fore;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System);
procedure Put
(Item : Num;
Fore : Field := Default_Fore;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Get
(From : String;
Item : out Num;
Last : out Positive);
Last : out Positive)
with
Global => null;
procedure Put
(To : out String;
Item : Num;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Global => null;
private
pragma Inline (Get);
......
gcc/ada/libgnat/a-tienio.ads
......@@ -28,28 +28,49 @@ package Ada.Text_IO.Enumeration_IO is
Default_Width : Field := 0;
Default_Setting : Type_Set := Upper_Case;
procedure Get (File : File_Type; Item : out Enum);
procedure Get (Item : out Enum);
procedure Get (File : File_Type; Item : out Enum) with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (In_Out => File_System);
procedure Get (Item : out Enum) with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Put
(File : File_Type;
Item : Enum;
Width : Field := Default_Width;
Set : Type_Set := Default_Setting);
Set : Type_Set := Default_Setting)
with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System);
procedure Put
(Item : Enum;
Width : Field := Default_Width;
Set : Type_Set := Default_Setting);
Set : Type_Set := Default_Setting)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Get
(From : String;
Item : out Enum;
Last : out Positive);
Last : out Positive)
with
Global => null;
procedure Put
(To : out String;
Item : Enum;
Set : Type_Set := Default_Setting);
Set : Type_Set := Default_Setting)
with
Global => null;
end Ada.Text_IO.Enumeration_IO;
gcc/ada/libgnat/a-tifiio.ads
......@@ -32,35 +32,58 @@ package Ada.Text_IO.Fixed_IO is
procedure Get
(File : File_Type;
Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (In_Out => File_System);
procedure Get
(Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Put
(File : File_Type;
Item : Num;
Fore : Field := Default_Fore;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System);
procedure Put
(Item : Num;
Fore : Field := Default_Fore;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Get
(From : String;
Item : out Num;
Last : out Positive);
Last : out Positive)
with
Global => null;
procedure Put
(To : out String;
Item : Num;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Global => null;
private
pragma Inline (Get);
......
gcc/ada/libgnat/a-tiflio.ads
......@@ -52,35 +52,58 @@ package Ada.Text_IO.Float_IO is
procedure Get
(File : File_Type;
Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (In_Out => File_System);
procedure Get
(Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Put
(File : File_Type;
Item : Num;
Fore : Field := Default_Fore;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System);
procedure Put
(Item : Num;
Fore : Field := Default_Fore;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Get
(From : String;
Item : out Num;
Last : out Positive);
Last : out Positive)
with
Global => null;
procedure Put
(To : out String;
Item : Num;
Aft : Field := Default_Aft;
Exp : Field := Default_Exp);
Exp : Field := Default_Exp)
with
Global => null;
private
pragma Inline (Get);
......
gcc/ada/libgnat/a-tiinio.ads
......@@ -51,32 +51,55 @@ package Ada.Text_IO.Integer_IO is
procedure Get
(File : File_Type;
Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (In_Out => File_System);
procedure Get
(Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Put
(File : File_Type;
Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base);
Base : Number_Base := Default_Base)
with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System);
procedure Put
(Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base);
Base : Number_Base := Default_Base)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Get
(From : String;
Item : out Num;
Last : out Positive);
Last : out Positive)
with
Global => null;
procedure Put
(To : out String;
Item : Num;
Base : Number_Base := Default_Base);
Base : Number_Base := Default_Base)
with
Global => null;
private
pragma Inline (Get);
......
gcc/ada/libgnat/a-timoio.ads
......@@ -51,32 +51,55 @@ package Ada.Text_IO.Modular_IO is
procedure Get
(File : File_Type;
Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Pre => Is_Open (File) and then Mode (File) = In_File,
Global => (In_Out => File_System);
procedure Get
(Item : out Num;
Width : Field := 0);
Width : Field := 0)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Put
(File : File_Type;
Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base);
Base : Number_Base := Default_Base)
with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System);
procedure Put
(Item : Num;
Width : Field := Default_Width;
Base : Number_Base := Default_Base);
Base : Number_Base := Default_Base)
with
Post =>
Line_Length'Old = Line_Length
and Page_Length'Old = Page_Length,
Global => (In_Out => File_System);
procedure Get
(From : String;
Item : out Num;
Last : out Positive);
Last : out Positive)
with
Global => null;
procedure Put
(To : out String;
Item : Num;
Base : Number_Base := Default_Base);
Base : Number_Base := Default_Base)
with
Global => null;
private
pragma Inline (Get);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment