[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