[gcc r11-6118] [Ada] Mark generic body outside of SPARK

[gcc r11-6118] [Ada] Mark generic body outside of SPARK

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:c507c83b324582dc05db91d332b0de4b25c85c07

commit r11-6118-gc507c83b324582dc05db91d332b0de4b25c85c07
Author: Yannick Moy <moy@adacore.com>
Date:   Fri Nov 27 10:13:23 2020 +0100

    [Ada] Mark generic body outside of SPARK
    
    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:
---
 gcc/ada/libgnat/a-tifiio.adb      | 2 +-
 gcc/ada/libgnat/a-tifiio.ads      | 2 +-
 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 0d9f6a55090..412740ed691 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 1acf67ab760..8a3886d30e6 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 ba96bd83f25..f50e4c92575 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