diff mbox series

[Ada] Mark generic body outside of SPARK

Message ID 20201215114241.GA35231@adacore.com
State New
Headers show
Series [Ada] Mark generic body outside of SPARK | expand

Commit Message

Pierre-Marie de Rodat Dec. 15, 2020, 11:42 a.m. UTC 
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.
diff mbox series

Patch

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;