From: Yannick Moy Date: Fri, 27 Nov 2020 09:13:23 +0000 (+0100) Subject: [Ada] Mark generic body outside of SPARK X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c507c83b324582dc05db91d332b0de4b25c85c07;p=gcc.git [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 --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