diff mbox series

[Ada] Mark generic body outside of SPARK

Message ID 20201216131534.GA69717@adacore.com
State New
Headers show
Series [Ada] Mark generic body outside of SPARK | expand

Commit Message

Pierre-Marie de Rodat Dec. 16, 2020, 1:15 p.m. UTC 
Unit Ada.Text_IO.Fixed_IO is now generic, which makes it necessary to
exclude the generic body from SPARK explicitly because it uses type
Long_Long_Float which is not supported in GNATprove. This ensures that
the unit can be instantiated from SPARK code.

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

gcc/ada/

	* libgnat/a-tifiio.adb: Mark body not in SPARK.
	* libgnat/a-tifiio.ads: Mark spec in SPARK.
	* libgnat/a-tifiio__128.adb: Mark body not in SPARK.
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/a-tifiio.adb b/gcc/ada/libgnat/a-tifiio.adb
--- a/gcc/ada/libgnat/a-tifiio.adb
+++ b/gcc/ada/libgnat/a-tifiio.adb
@@ -162,7 +162,7 @@  with System.Val_Fixed_32; use System.Val_Fixed_32;
 with System.Val_Fixed_64; use System.Val_Fixed_64;
 with System.Val_LLF;      use System.Val_LLF;
 
-package body Ada.Text_IO.Fixed_IO is
+package body Ada.Text_IO.Fixed_IO with SPARK_Mode => Off is
 
    --  Note: we still use the floating-point I/O routines for types whose small
    --  is not the ratio of two sufficiently small integers. This will result in


diff --git a/gcc/ada/libgnat/a-tifiio.ads b/gcc/ada/libgnat/a-tifiio.ads
--- a/gcc/ada/libgnat/a-tifiio.ads
+++ b/gcc/ada/libgnat/a-tifiio.ads
@@ -23,7 +23,7 @@ 
 private generic
    type Num is delta <>;
 
-package Ada.Text_IO.Fixed_IO is
+package Ada.Text_IO.Fixed_IO with SPARK_Mode => On is
 
    Default_Fore : Field := Num'Fore;
    Default_Aft  : Field := Num'Aft;


diff --git a/gcc/ada/libgnat/a-tifiio__128.adb b/gcc/ada/libgnat/a-tifiio__128.adb
--- a/gcc/ada/libgnat/a-tifiio__128.adb
+++ b/gcc/ada/libgnat/a-tifiio__128.adb
@@ -164,7 +164,7 @@  with System.Val_Fixed_64;  use System.Val_Fixed_64;
 with System.Val_Fixed_128; use System.Val_Fixed_128;
 with System.Val_LLF;       use System.Val_LLF;
 
-package body Ada.Text_IO.Fixed_IO is
+package body Ada.Text_IO.Fixed_IO with SPARK_Mode => Off is
 
    --  Note: we still use the floating-point I/O routines for types whose small
    --  is not the ratio of two sufficiently small integers. This will result in