diff --git a/gcc/ada/libgnat/a-tiflio.adb b/gcc/ada/libgnat/a-tiflio.adb
index 0daa0442bd2aa6a1f40224bf8ff0e6d0e6e860cb..8da79f102f105bcfbbab52a1ff947d19b039160a 100644
--- a/gcc/ada/libgnat/a-tiflio.adb
+++ b/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;
 
diff --git a/gcc/ada/libgnat/a-tiflio.ads b/gcc/ada/libgnat/a-tiflio.ads
index bd4c64f6474fde67cc66be08a84f858cbe44d4d2..d61b9e75ce768c1d7764616d5d0cde33192e8dd8 100644
--- a/gcc/ada/libgnat/a-tiflio.ads
+++ b/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;