From 1851d3cef24d4cbc3b55305c75c04a2ce9667315 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Wed, 25 Nov 2020 10:33:54 +0100 Subject: [PATCH] [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. --- gcc/ada/libgnat/a-tiflio.adb | 2 +- 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 0daa0442bd2..8da79f102f1 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 bd4c64f6474..d61b9e75ce7 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; -- 2.30.2