diff options
| -rw-r--r-- | gcc/ada/libgnat/a-tifiio.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-tifiio.ads | 2 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-tifiio__128.adb | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/gcc/ada/libgnat/a-tifiio.adb b/gcc/ada/libgnat/a-tifiio.adb index 0d9f6a5..412740e 100644 --- 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 index 1acf67a..8a3886d 100644 --- 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 index ba96bd8..f50e4c9 100644 --- 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 |