mirror/gcc
2
0
Fork 0
mirror of git://gcc.gnu.org/git/gcc.git synced 2025-04-23 01:30:29 +08:00
Code Issues Packages Projects Releases Wiki Activity

[Ada] Mark generic body outside of SPARK

Browse Source 
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.
This commit is contained in:
Yannick Moy 2020-11-27 10:13:23 +01:00 committed by Pierre-Marie de Rodat
parent 94117322e6
commit c507c83b32
3 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
gcc/ada/libgnat/a-tifiio.adb
View File

@ -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

2
gcc/ada/libgnat/a-tifiio.ads
View File

@ -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;

2
gcc/ada/libgnat/a-tifiio__128.adb
View File

@ -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