[Ada] Mark generic body outside of SPARK

gcc/ada/

	* libgnat/a-tiflio.adb: Mark body not in SPARK.
	* libgnat/a-tiflio.ads: Mark spec in SPARK.

gcc/ada/libgnat/a-tiflio.adb

@@ -31,7 +31,7 @@
 
 with Ada.Text_IO.Float_Aux;
 
-package body Ada.Text_IO.Float_IO is
+package body Ada.Text_IO.Float_IO with SPARK_Mode => Off is
 
    package Aux renames Ada.Text_IO.Float_Aux;
 

gcc/ada/libgnat/a-tiflio.ads

@@ -43,7 +43,7 @@
 private generic
    type Num is digits <>;
 
-package Ada.Text_IO.Float_IO is
+package Ada.Text_IO.Float_IO with SPARK_Mode => On is
 
    Default_Fore : Field := 2;
    Default_Aft  : Field := Num'Digits - 1;