diff options
| author | Yannick Moy <moy@adacore.com> | 2020-11-27 10:13:23 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-12-16 08:01:00 -0500 |
| commit | c507c83b324582dc05db91d332b0de4b25c85c07 (patch) | |
| tree | 0fa15185b35a4bc6107b1f3f6f3626bba3760ebc /gcc | |
| parent | 94117322e68f29677f5a7088fc83f57e824ca8a7 (diff) | |
| download | gcc-c507c83b324582dc05db91d332b0de4b25c85c07.zip gcc-c507c83b324582dc05db91d332b0de4b25c85c07.tar.gz gcc-c507c83b324582dc05db91d332b0de4b25c85c07.tar.bz2 | |
[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.
Diffstat (limited to 'gcc')
| -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 |