diff options
| author | Yannick Moy <moy@adacore.com> | 2020-11-25 10:33:54 +0100 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-12-15 06:41:54 -0500 |
| commit | 1851d3cef24d4cbc3b55305c75c04a2ce9667315 (patch) | |
| tree | 5f99e938d4b73a15b464a6daaa45d42c5cc6c596 | |
| parent | d79e7af5ff74c714b15d0cd123752cc4714e4dc6 (diff) | |
| download | gcc-1851d3cef24d4cbc3b55305c75c04a2ce9667315.zip gcc-1851d3cef24d4cbc3b55305c75c04a2ce9667315.tar.gz gcc-1851d3cef24d4cbc3b55305c75c04a2ce9667315.tar.bz2 | |
[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.
| -rw-r--r-- | gcc/ada/libgnat/a-tiflio.adb | 2 | ||||
| -rw-r--r-- | gcc/ada/libgnat/a-tiflio.ads | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/a-tiflio.adb b/gcc/ada/libgnat/a-tiflio.adb index 0daa044..8da79f1 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 bd4c64f64..d61b9e7 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; |