[gcc r12-3711] [Ada] Add SPARK_Mode => Off to System.File_Control_Block
Pierre-Marie de Rodat
pmderodat@gcc.gnu.org
Mon Sep 20 13:05:44 GMT 2021
https://gcc.gnu.org/g:9613900aef1cdb5c5c3b867825b6295c0b00f4cc
commit r12-3711-g9613900aef1cdb5c5c3b867825b6295c0b00f4cc
Author: Claire Dross <dross@adacore.com>
Date: Tue Jun 29 10:38:31 2021 +0200
[Ada] Add SPARK_Mode => Off to System.File_Control_Block
gcc/ada/
* libgnat/s-ficobl.ads: The entire package has a SPARK_Mode =>
Off aspect.
Diff:
---
gcc/ada/libgnat/s-ficobl.ads | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/gcc/ada/libgnat/s-ficobl.ads b/gcc/ada/libgnat/s-ficobl.ads
index 6fff2daa8c3..4e970791c7e 100644
--- a/gcc/ada/libgnat/s-ficobl.ads
+++ b/gcc/ada/libgnat/s-ficobl.ads
@@ -39,7 +39,7 @@ with Ada.Streams;
with Interfaces.C_Streams;
with System.CRTL;
-package System.File_Control_Block is
+package System.File_Control_Block with SPARK_Mode => Off is
pragma Preelaborate;
----------------------------
More information about the Gcc-cvs
mailing list