projects / platform / upstream / gcc.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: c5049df)
[Ada] Add SPARK_Mode => Off to System.File_Control_Block
authorClaire Dross <dross@adacore.com>
Tue, 29 Jun 2021 08:38:31 +0000 (10:38 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Mon, 20 Sep 2021 12:31:36 +0000 (12:31 +0000)
gcc/ada/

* libgnat/s-ficobl.ads: The entire package has a SPARK_Mode =>
Off aspect.

gcc/ada/libgnat/s-ficobl.ads patch | blob | history

diff --git a/gcc/ada/libgnat/s-ficobl.ads b/gcc/ada/libgnat/s-ficobl.ads
index 6fff2da..4e97079 100644 (file)
--- 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;
 
    ----------------------------
Domain: System / Toolchain;