[Ada] Add contracts to Ada.Text_IO for SPARK

[Pierre-Marie de Rodat]

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.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: patch.diff.gz
Type: application/gzip
Size: 3501 bytes
Desc: not available
URL: <http://gcc.gnu.org/pipermail/gcc-patches/attachments/20190705/3caf68c2/attachment.gz>