[Ada] Add contracts to Ada.Text_IO for SPARK

Programming / Compilers / GCC - pmderodat [138bc75d-0d04-0410-961f-82ee72b054a4] - 5 July 2019 07:03 EDT

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

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.

30fb27b121a [Ada] Add contracts to Ada.Text_IO for SPARK
gcc/ada/ChangeLog | 16 ++
gcc/ada/libgnat/a-textio.adb | 13 +-
gcc/ada/libgnat/a-textio.ads | 466 +++++++++++++++++++++++++++++++++----------
gcc/ada/libgnat/a-tideio.ads | 35 +++-
gcc/ada/libgnat/a-tienio.ads | 33 ++-
gcc/ada/libgnat/a-tifiio.ads | 35 +++-
gcc/ada/libgnat/a-tiflio.ads | 35 +++-
gcc/ada/libgnat/a-tiinio.ads | 35 +++-
gcc/ada/libgnat/a-timoio.ads | 35 +++-
9 files changed, 561 insertions(+), 142 deletions(-)

Upstream: gcc.gnu.org


  • Share