* [Ada] Mark generic body outside of SPARK
@ 2020-12-15 11:42 Pierre-Marie de Rodat
0 siblings, 0 replies; 2+ messages in thread
From: Pierre-Marie de Rodat @ 2020-12-15 11:42 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 374 bytes --]
New body for Ada.Text_IO.Float_IO makes explicit use of Long_Long_Float
which is not supported by GNATprove for now. Exclude that generic body
from SPARK explicitly so that the unit can be instantiated from SPARK
code.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/a-tiflio.adb: Mark body not in SPARK.
* libgnat/a-tiflio.ads: Mark spec in SPARK.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 720 bytes --]
diff --git a/gcc/ada/libgnat/a-tiflio.adb b/gcc/ada/libgnat/a-tiflio.adb
--- 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
--- 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;
^ permalink raw reply [flat|nested] 2+ messages in thread
* [Ada] Mark generic body outside of SPARK
@ 2020-12-16 13:15 Pierre-Marie de Rodat
0 siblings, 0 replies; 2+ messages in thread
From: Pierre-Marie de Rodat @ 2020-12-16 13:15 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 464 bytes --]
Unit Ada.Text_IO.Fixed_IO is now generic, which makes it necessary to
exclude the generic body from SPARK explicitly because it uses type
Long_Long_Float which is not supported in GNATprove. This ensures that
the unit can be instantiated from SPARK code.
Tested on x86_64-pc-linux-gnu, committed on trunk
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.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1557 bytes --]
diff --git a/gcc/ada/libgnat/a-tifiio.adb b/gcc/ada/libgnat/a-tifiio.adb
--- 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
--- 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
--- 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
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2020-12-16 13:15 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-12-15 11:42 [Ada] Mark generic body outside of SPARK Pierre-Marie de Rodat
2020-12-16 13:15 Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).