[gcc/devel/c++-modules] [Ada] Mark standard containers as not in SPARK

Nathan Sidwell nathan@gcc.gnu.org
Wed Jul 15 18:46:45 GMT 2020 

https://gcc.gnu.org/g:3221be144431dae561be518c1411849fa65ac486

commit 3221be144431dae561be518c1411849fa65ac486
Author: Yannick Moy <moy@adacore.com>
Date:   Tue Jun 2 14:16:25 2020 +0200

    [Ada] Mark standard containers as not in SPARK
    
    gcc/ada/
    
            * libgnat/a-cbdlli.adb, libgnat/a-cbdlli.ads,
            libgnat/a-cbhama.adb, libgnat/a-cbhama.ads,
            libgnat/a-cbhase.adb, libgnat/a-cbhase.ads,
            libgnat/a-cbmutr.adb, libgnat/a-cbmutr.ads,
            libgnat/a-cborma.adb, libgnat/a-cborma.ads,
            libgnat/a-cborse.adb, libgnat/a-cborse.ads,
            libgnat/a-cbprqu.adb, libgnat/a-cbprqu.ads,
            libgnat/a-cbsyqu.adb, libgnat/a-cbsyqu.ads,
            libgnat/a-cdlili.adb, libgnat/a-cdlili.ads,
            libgnat/a-cidlli.adb, libgnat/a-cidlli.ads,
            libgnat/a-cihama.adb, libgnat/a-cihama.ads,
            libgnat/a-cihase.adb, libgnat/a-cihase.ads,
            libgnat/a-cimutr.adb, libgnat/a-cimutr.ads,
            libgnat/a-ciorma.adb, libgnat/a-ciorma.ads,
            libgnat/a-ciormu.adb, libgnat/a-ciormu.ads,
            libgnat/a-ciorse.adb, libgnat/a-ciorse.ads,
            libgnat/a-cohama.adb, libgnat/a-cohama.ads,
            libgnat/a-cohase.adb, libgnat/a-cohase.ads,
            libgnat/a-coinve.adb, libgnat/a-coinve.ads,
            libgnat/a-comutr.adb, libgnat/a-comutr.ads,
            libgnat/a-convec.adb, libgnat/a-convec.ads,
            libgnat/a-coorma.adb, libgnat/a-coorma.ads,
            libgnat/a-coormu.adb, libgnat/a-coormu.ads,
            libgnat/a-coorse.adb, libgnat/a-coorse.ads: Add SPARK_Mode =>
            Off.

Diff:
---
 gcc/ada/libgnat/a-cbdlli.adb | 4 +++-
 gcc/ada/libgnat/a-cbdlli.ads | 4 +++-
 gcc/ada/libgnat/a-cbhama.adb | 4 +++-
 gcc/ada/libgnat/a-cbhama.ads | 4 +++-
 gcc/ada/libgnat/a-cbhase.adb | 4 +++-
 gcc/ada/libgnat/a-cbhase.ads | 4 +++-
 gcc/ada/libgnat/a-cbmutr.adb | 4 +++-
 gcc/ada/libgnat/a-cbmutr.ads | 4 +++-
 gcc/ada/libgnat/a-cborma.adb | 4 +++-
 gcc/ada/libgnat/a-cborma.ads | 4 +++-
 gcc/ada/libgnat/a-cborse.adb | 4 +++-
 gcc/ada/libgnat/a-cborse.ads | 4 +++-
 gcc/ada/libgnat/a-cbprqu.adb | 4 +++-
 gcc/ada/libgnat/a-cbprqu.ads | 4 +++-
 gcc/ada/libgnat/a-cbsyqu.adb | 4 +++-
 gcc/ada/libgnat/a-cbsyqu.ads | 4 +++-
 gcc/ada/libgnat/a-cdlili.adb | 4 +++-
 gcc/ada/libgnat/a-cdlili.ads | 4 +++-
 gcc/ada/libgnat/a-cidlli.adb | 4 +++-
 gcc/ada/libgnat/a-cidlli.ads | 4 +++-
 gcc/ada/libgnat/a-cihama.adb | 4 +++-
 gcc/ada/libgnat/a-cihama.ads | 4 +++-
 gcc/ada/libgnat/a-cihase.adb | 4 +++-
 gcc/ada/libgnat/a-cihase.ads | 4 +++-
 gcc/ada/libgnat/a-cimutr.adb | 4 +++-
 gcc/ada/libgnat/a-cimutr.ads | 4 +++-
 gcc/ada/libgnat/a-ciorma.adb | 4 +++-
 gcc/ada/libgnat/a-ciorma.ads | 4 +++-
 gcc/ada/libgnat/a-ciormu.adb | 4 +++-
 gcc/ada/libgnat/a-ciormu.ads | 4 +++-
 gcc/ada/libgnat/a-ciorse.adb | 4 +++-
 gcc/ada/libgnat/a-ciorse.ads | 4 +++-
 gcc/ada/libgnat/a-cohama.adb | 4 +++-
 gcc/ada/libgnat/a-cohama.ads | 4 +++-
 gcc/ada/libgnat/a-cohase.adb | 4 +++-
 gcc/ada/libgnat/a-cohase.ads | 4 +++-
 gcc/ada/libgnat/a-coinve.adb | 4 +++-
 gcc/ada/libgnat/a-coinve.ads | 4 +++-
 gcc/ada/libgnat/a-comutr.adb | 4 +++-
 gcc/ada/libgnat/a-comutr.ads | 4 +++-
 gcc/ada/libgnat/a-convec.adb | 4 +++-
 gcc/ada/libgnat/a-convec.ads | 4 +++-
 gcc/ada/libgnat/a-coorma.adb | 4 +++-
 gcc/ada/libgnat/a-coorma.ads | 4 +++-
 gcc/ada/libgnat/a-coormu.adb | 4 +++-
 gcc/ada/libgnat/a-coormu.ads | 4 +++-
 gcc/ada/libgnat/a-coorse.adb | 4 +++-
 gcc/ada/libgnat/a-coorse.ads | 4 +++-
 48 files changed, 144 insertions(+), 48 deletions(-)

diff --git a/gcc/ada/libgnat/a-cbdlli.adb b/gcc/ada/libgnat/a-cbdlli.adb
index 1b3a88cd60e..0f0c872e887 100644
--- a/gcc/ada/libgnat/a-cbdlli.adb
+++ b/gcc/ada/libgnat/a-cbdlli.adb
@@ -29,7 +29,9 @@
 
 with System; use type System.Address;
 
-package body Ada.Containers.Bounded_Doubly_Linked_Lists is
+package body Ada.Containers.Bounded_Doubly_Linked_Lists with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cbdlli.ads b/gcc/ada/libgnat/a-cbdlli.ads
index 0103a03e688..74639cf07d2 100644
--- a/gcc/ada/libgnat/a-cbdlli.ads
+++ b/gcc/ada/libgnat/a-cbdlli.ads
@@ -43,7 +43,9 @@ generic
    with function "=" (Left, Right : Element_Type)
       return Boolean is <>;
 
-package Ada.Containers.Bounded_Doubly_Linked_Lists is
+package Ada.Containers.Bounded_Doubly_Linked_Lists with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Pure;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cbhama.adb b/gcc/ada/libgnat/a-cbhama.adb
index b76bd623cd7..1881db212bc 100644
--- a/gcc/ada/libgnat/a-cbhama.adb
+++ b/gcc/ada/libgnat/a-cbhama.adb
@@ -39,7 +39,9 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Bounded_Hashed_Maps is
+package body Ada.Containers.Bounded_Hashed_Maps with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cbhama.ads b/gcc/ada/libgnat/a-cbhama.ads
index cf76fbb25e2..86fed4e6997 100644
--- a/gcc/ada/libgnat/a-cbhama.ads
+++ b/gcc/ada/libgnat/a-cbhama.ads
@@ -45,7 +45,9 @@ generic
    with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Bounded_Hashed_Maps is
+package Ada.Containers.Bounded_Hashed_Maps with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Pure;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cbhase.adb b/gcc/ada/libgnat/a-cbhase.adb
index 8a786f1f68e..a332bd74a7f 100644
--- a/gcc/ada/libgnat/a-cbhase.adb
+++ b/gcc/ada/libgnat/a-cbhase.adb
@@ -39,7 +39,9 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Bounded_Hashed_Sets is
+package body Ada.Containers.Bounded_Hashed_Sets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cbhase.ads b/gcc/ada/libgnat/a-cbhase.ads
index 663dcb3eaf5..01903c74a0c 100644
--- a/gcc/ada/libgnat/a-cbhase.ads
+++ b/gcc/ada/libgnat/a-cbhase.ads
@@ -48,7 +48,9 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Bounded_Hashed_Sets is
+package Ada.Containers.Bounded_Hashed_Sets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Pure;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cbmutr.adb b/gcc/ada/libgnat/a-cbmutr.adb
index f9048b09c2f..58db8cf4471 100644
--- a/gcc/ada/libgnat/a-cbmutr.adb
+++ b/gcc/ada/libgnat/a-cbmutr.adb
@@ -30,7 +30,9 @@
 with Ada.Finalization;
 with System; use type System.Address;
 
-package body Ada.Containers.Bounded_Multiway_Trees is
+package body Ada.Containers.Bounded_Multiway_Trees with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cbmutr.ads b/gcc/ada/libgnat/a-cbmutr.ads
index 8008e1dcf58..653407bfcdc 100644
--- a/gcc/ada/libgnat/a-cbmutr.ads
+++ b/gcc/ada/libgnat/a-cbmutr.ads
@@ -41,7 +41,9 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Bounded_Multiway_Trees is
+package Ada.Containers.Bounded_Multiway_Trees with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Pure;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cborma.adb b/gcc/ada/libgnat/a-cborma.adb
index 1e384d777e0..6f59471cb7c 100644
--- a/gcc/ada/libgnat/a-cborma.adb
+++ b/gcc/ada/libgnat/a-cborma.adb
@@ -39,7 +39,9 @@ pragma Elaborate_All
 
 with System; use type System.Address;
 
-package body Ada.Containers.Bounded_Ordered_Maps is
+package body Ada.Containers.Bounded_Ordered_Maps with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cborma.ads b/gcc/ada/libgnat/a-cborma.ads
index 1cfc41229ed..c199a09efbf 100644
--- a/gcc/ada/libgnat/a-cborma.ads
+++ b/gcc/ada/libgnat/a-cborma.ads
@@ -44,7 +44,9 @@ generic
    with function "<" (Left, Right : Key_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Bounded_Ordered_Maps is
+package Ada.Containers.Bounded_Ordered_Maps with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Pure;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cborse.adb b/gcc/ada/libgnat/a-cborse.adb
index af5efc1f5ca..af4f87f157d 100644
--- a/gcc/ada/libgnat/a-cborse.adb
+++ b/gcc/ada/libgnat/a-cborse.adb
@@ -42,7 +42,9 @@ pragma Elaborate_All
 
 with System; use type System.Address;
 
-package body Ada.Containers.Bounded_Ordered_Sets is
+package body Ada.Containers.Bounded_Ordered_Sets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cborse.ads b/gcc/ada/libgnat/a-cborse.ads
index a119c821e44..52b8786f3c8 100644
--- a/gcc/ada/libgnat/a-cborse.ads
+++ b/gcc/ada/libgnat/a-cborse.ads
@@ -44,7 +44,9 @@ generic
    with function "<" (Left, Right : Element_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Bounded_Ordered_Sets is
+package Ada.Containers.Bounded_Ordered_Sets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Pure;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cbprqu.adb b/gcc/ada/libgnat/a-cbprqu.adb
index 27b5bd3e829..2e972912548 100644
--- a/gcc/ada/libgnat/a-cbprqu.adb
+++ b/gcc/ada/libgnat/a-cbprqu.adb
@@ -27,7 +27,9 @@
 -- This unit was originally developed by Matthew J Heaney.                  --
 ------------------------------------------------------------------------------
 
-package body Ada.Containers.Bounded_Priority_Queues is
+package body Ada.Containers.Bounded_Priority_Queues with
+  SPARK_Mode => Off
+is
 
    package body Implementation is
 
diff --git a/gcc/ada/libgnat/a-cbprqu.ads b/gcc/ada/libgnat/a-cbprqu.ads
index e5a9b66b436..6259a472a72 100644
--- a/gcc/ada/libgnat/a-cbprqu.ads
+++ b/gcc/ada/libgnat/a-cbprqu.ads
@@ -51,7 +51,9 @@ generic
    Default_Capacity : Count_Type;
    Default_Ceiling  : System.Any_Priority := System.Priority'Last;
 
-package Ada.Containers.Bounded_Priority_Queues is
+package Ada.Containers.Bounded_Priority_Queues with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
 
diff --git a/gcc/ada/libgnat/a-cbsyqu.adb b/gcc/ada/libgnat/a-cbsyqu.adb
index 62cad5de8f6..abb0e7940ba 100644
--- a/gcc/ada/libgnat/a-cbsyqu.adb
+++ b/gcc/ada/libgnat/a-cbsyqu.adb
@@ -27,7 +27,9 @@
 -- This unit was originally developed by Matthew J Heaney.                  --
 ------------------------------------------------------------------------------
 
-package body Ada.Containers.Bounded_Synchronized_Queues is
+package body Ada.Containers.Bounded_Synchronized_Queues with
+  SPARK_Mode => Off
+is
 
    package body Implementation is
 
diff --git a/gcc/ada/libgnat/a-cbsyqu.ads b/gcc/ada/libgnat/a-cbsyqu.ads
index 07fe84b3388..61504fa33e7 100644
--- a/gcc/ada/libgnat/a-cbsyqu.ads
+++ b/gcc/ada/libgnat/a-cbsyqu.ads
@@ -41,7 +41,9 @@ generic
    Default_Capacity : Count_Type;
    Default_Ceiling  : System.Any_Priority := System.Priority'Last;
 
-package Ada.Containers.Bounded_Synchronized_Queues is
+package Ada.Containers.Bounded_Synchronized_Queues with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
 
diff --git a/gcc/ada/libgnat/a-cdlili.adb b/gcc/ada/libgnat/a-cdlili.adb
index 73c7980a157..a668db11bb1 100644
--- a/gcc/ada/libgnat/a-cdlili.adb
+++ b/gcc/ada/libgnat/a-cdlili.adb
@@ -31,7 +31,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Doubly_Linked_Lists is
+package body Ada.Containers.Doubly_Linked_Lists with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cdlili.ads b/gcc/ada/libgnat/a-cdlili.ads
index 424a346c0df..89216e03226 100644
--- a/gcc/ada/libgnat/a-cdlili.ads
+++ b/gcc/ada/libgnat/a-cdlili.ads
@@ -43,7 +43,9 @@ generic
    with function "=" (Left, Right : Element_Type)
       return Boolean is <>;
 
-package Ada.Containers.Doubly_Linked_Lists is
+package Ada.Containers.Doubly_Linked_Lists with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cidlli.adb b/gcc/ada/libgnat/a-cidlli.adb
index a086935dd3a..0898db8c401 100644
--- a/gcc/ada/libgnat/a-cidlli.adb
+++ b/gcc/ada/libgnat/a-cidlli.adb
@@ -31,7 +31,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Doubly_Linked_Lists is
+package body Ada.Containers.Indefinite_Doubly_Linked_Lists with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cidlli.ads b/gcc/ada/libgnat/a-cidlli.ads
index 1111bbbb1dc..e9220a6e257 100644
--- a/gcc/ada/libgnat/a-cidlli.ads
+++ b/gcc/ada/libgnat/a-cidlli.ads
@@ -43,7 +43,9 @@ generic
    with function "=" (Left, Right : Element_Type)
       return Boolean is <>;
 
-package Ada.Containers.Indefinite_Doubly_Linked_Lists is
+package Ada.Containers.Indefinite_Doubly_Linked_Lists with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cihama.adb b/gcc/ada/libgnat/a-cihama.adb
index 7c4d427ca24..9f5aed7b02b 100644
--- a/gcc/ada/libgnat/a-cihama.adb
+++ b/gcc/ada/libgnat/a-cihama.adb
@@ -39,7 +39,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Hashed_Maps is
+package body Ada.Containers.Indefinite_Hashed_Maps with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cihama.ads b/gcc/ada/libgnat/a-cihama.ads
index 4d9233a1d7e..fb6f4e00990 100644
--- a/gcc/ada/libgnat/a-cihama.ads
+++ b/gcc/ada/libgnat/a-cihama.ads
@@ -45,7 +45,9 @@ generic
    with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Indefinite_Hashed_Maps is
+package Ada.Containers.Indefinite_Hashed_Maps with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cihase.adb b/gcc/ada/libgnat/a-cihase.adb
index 3d5af6a1769..b91532dc974 100644
--- a/gcc/ada/libgnat/a-cihase.adb
+++ b/gcc/ada/libgnat/a-cihase.adb
@@ -41,7 +41,9 @@ with Ada.Containers.Prime_Numbers;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Hashed_Sets is
+package body Ada.Containers.Indefinite_Hashed_Sets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cihase.ads b/gcc/ada/libgnat/a-cihase.ads
index e6dcef69b60..926e07f1faa 100644
--- a/gcc/ada/libgnat/a-cihase.ads
+++ b/gcc/ada/libgnat/a-cihase.ads
@@ -48,7 +48,9 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Indefinite_Hashed_Sets is
+package Ada.Containers.Indefinite_Hashed_Sets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cimutr.adb b/gcc/ada/libgnat/a-cimutr.adb
index ac7e534380a..293275ae5a9 100644
--- a/gcc/ada/libgnat/a-cimutr.adb
+++ b/gcc/ada/libgnat/a-cimutr.adb
@@ -31,7 +31,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Multiway_Trees is
+package body Ada.Containers.Indefinite_Multiway_Trees with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cimutr.ads b/gcc/ada/libgnat/a-cimutr.ads
index 5d213250ff0..474a1b57aa9 100644
--- a/gcc/ada/libgnat/a-cimutr.ads
+++ b/gcc/ada/libgnat/a-cimutr.ads
@@ -42,7 +42,9 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Indefinite_Multiway_Trees is
+package Ada.Containers.Indefinite_Multiway_Trees with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-ciorma.adb b/gcc/ada/libgnat/a-ciorma.adb
index 25cf67445f1..86cd01f09c8 100644
--- a/gcc/ada/libgnat/a-ciorma.adb
+++ b/gcc/ada/libgnat/a-ciorma.adb
@@ -39,7 +39,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Keys);
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Ordered_Maps is
+package body Ada.Containers.Indefinite_Ordered_Maps with
+  SPARK_Mode => Off
+is
    pragma Suppress (All_Checks);
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-ciorma.ads b/gcc/ada/libgnat/a-ciorma.ads
index bc4581dd513..a7799a613a6 100644
--- a/gcc/ada/libgnat/a-ciorma.ads
+++ b/gcc/ada/libgnat/a-ciorma.ads
@@ -44,7 +44,9 @@ generic
    with function "<" (Left, Right : Key_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Indefinite_Ordered_Maps is
+package Ada.Containers.Indefinite_Ordered_Maps with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-ciormu.adb b/gcc/ada/libgnat/a-ciormu.adb
index 62993388a43..110d734db59 100644
--- a/gcc/ada/libgnat/a-ciormu.adb
+++ b/gcc/ada/libgnat/a-ciormu.adb
@@ -40,7 +40,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Set_Operations);
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Ordered_Multisets is
+package body Ada.Containers.Indefinite_Ordered_Multisets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-ciormu.ads b/gcc/ada/libgnat/a-ciormu.ads
index ad4e1b247ee..474ccc75e0d 100644
--- a/gcc/ada/libgnat/a-ciormu.ads
+++ b/gcc/ada/libgnat/a-ciormu.ads
@@ -43,7 +43,9 @@ generic
    with function "<" (Left, Right : Element_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Indefinite_Ordered_Multisets is
+package Ada.Containers.Indefinite_Ordered_Multisets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-ciorse.adb b/gcc/ada/libgnat/a-ciorse.adb
index f9647a2cf40..772061d886c 100644
--- a/gcc/ada/libgnat/a-ciorse.adb
+++ b/gcc/ada/libgnat/a-ciorse.adb
@@ -42,7 +42,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Ordered_Sets is
+package body Ada.Containers.Indefinite_Ordered_Sets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-ciorse.ads b/gcc/ada/libgnat/a-ciorse.ads
index 26cda02a5bf..1eb8135ff5c 100644
--- a/gcc/ada/libgnat/a-ciorse.ads
+++ b/gcc/ada/libgnat/a-ciorse.ads
@@ -44,7 +44,9 @@ generic
    with function "<" (Left, Right : Element_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Indefinite_Ordered_Sets is
+package Ada.Containers.Indefinite_Ordered_Sets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cohama.adb b/gcc/ada/libgnat/a-cohama.adb
index f5424623cf7..7f2d8e16ab5 100644
--- a/gcc/ada/libgnat/a-cohama.adb
+++ b/gcc/ada/libgnat/a-cohama.adb
@@ -39,7 +39,9 @@ with Ada.Containers.Helpers; use Ada.Containers.Helpers;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Hashed_Maps is
+package body Ada.Containers.Hashed_Maps with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cohama.ads b/gcc/ada/libgnat/a-cohama.ads
index 3cc923971df..9d927bd992b 100644
--- a/gcc/ada/libgnat/a-cohama.ads
+++ b/gcc/ada/libgnat/a-cohama.ads
@@ -88,7 +88,9 @@ generic
    --  map values returns an unspecified value. The exact arguments and number
    --  of calls of this generic formal function by the function "=" on map
    --  values are unspecified.
-package Ada.Containers.Hashed_Maps is
+package Ada.Containers.Hashed_Maps with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-cohase.adb b/gcc/ada/libgnat/a-cohase.adb
index 45a1b2e0294..bc4e53f68f3 100644
--- a/gcc/ada/libgnat/a-cohase.adb
+++ b/gcc/ada/libgnat/a-cohase.adb
@@ -41,7 +41,9 @@ with Ada.Containers.Prime_Numbers;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Hashed_Sets is
+package body Ada.Containers.Hashed_Sets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-cohase.ads b/gcc/ada/libgnat/a-cohase.ads
index 523e55468d0..3645ed07124 100644
--- a/gcc/ada/libgnat/a-cohase.ads
+++ b/gcc/ada/libgnat/a-cohase.ads
@@ -48,7 +48,9 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Hashed_Sets is
+package Ada.Containers.Hashed_Sets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-coinve.adb b/gcc/ada/libgnat/a-coinve.adb
index 85c30fa1832..79e36aea659 100644
--- a/gcc/ada/libgnat/a-coinve.adb
+++ b/gcc/ada/libgnat/a-coinve.adb
@@ -32,7 +32,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Indefinite_Vectors is
+package body Ada.Containers.Indefinite_Vectors with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-coinve.ads b/gcc/ada/libgnat/a-coinve.ads
index 2d5443892f7..075a1843319 100644
--- a/gcc/ada/libgnat/a-coinve.ads
+++ b/gcc/ada/libgnat/a-coinve.ads
@@ -43,7 +43,9 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Indefinite_Vectors is
+package Ada.Containers.Indefinite_Vectors with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-comutr.adb b/gcc/ada/libgnat/a-comutr.adb
index 6468839e294..76ff7515616 100644
--- a/gcc/ada/libgnat/a-comutr.adb
+++ b/gcc/ada/libgnat/a-comutr.adb
@@ -32,7 +32,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Multiway_Trees is
+package body Ada.Containers.Multiway_Trees with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-comutr.ads b/gcc/ada/libgnat/a-comutr.ads
index 89e57978212..46934a113c0 100644
--- a/gcc/ada/libgnat/a-comutr.ads
+++ b/gcc/ada/libgnat/a-comutr.ads
@@ -42,7 +42,9 @@ generic
 
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Multiway_Trees is
+package Ada.Containers.Multiway_Trees with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-convec.adb b/gcc/ada/libgnat/a-convec.adb
index 197271b87c7..c4d1406383e 100644
--- a/gcc/ada/libgnat/a-convec.adb
+++ b/gcc/ada/libgnat/a-convec.adb
@@ -32,7 +32,9 @@ with Ada.Unchecked_Deallocation;
 
 with System; use type System.Address;
 
-package body Ada.Containers.Vectors is
+package body Ada.Containers.Vectors with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-convec.ads b/gcc/ada/libgnat/a-convec.ads
index 8ad31a2ec09..7b2e1760834 100644
--- a/gcc/ada/libgnat/a-convec.ads
+++ b/gcc/ada/libgnat/a-convec.ads
@@ -70,7 +70,9 @@ generic
    --  number of calls of this generic formal function by the functions defined
    --  to use it are unspecified.
 
-package Ada.Containers.Vectors is
+package Ada.Containers.Vectors with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-coorma.adb b/gcc/ada/libgnat/a-coorma.adb
index 9bad901259a..4106d58ff4e 100644
--- a/gcc/ada/libgnat/a-coorma.adb
+++ b/gcc/ada/libgnat/a-coorma.adb
@@ -39,7 +39,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Keys);
 
 with System; use type System.Address;
 
-package body Ada.Containers.Ordered_Maps is
+package body Ada.Containers.Ordered_Maps with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-coorma.ads b/gcc/ada/libgnat/a-coorma.ads
index 02d97e416b5..e2d5e1e3e09 100644
--- a/gcc/ada/libgnat/a-coorma.ads
+++ b/gcc/ada/libgnat/a-coorma.ads
@@ -44,7 +44,9 @@ generic
    with function "<" (Left, Right : Key_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Ordered_Maps is
+package Ada.Containers.Ordered_Maps with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-coormu.adb b/gcc/ada/libgnat/a-coormu.adb
index 66cc77ed376..c02a9f1540e 100644
--- a/gcc/ada/libgnat/a-coormu.adb
+++ b/gcc/ada/libgnat/a-coormu.adb
@@ -40,7 +40,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Set_Operations);
 
 with System; use type System.Address;
 
-package body Ada.Containers.Ordered_Multisets is
+package body Ada.Containers.Ordered_Multisets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-coormu.ads b/gcc/ada/libgnat/a-coormu.ads
index cdaee8526ed..9c6c3ae8d98 100644
--- a/gcc/ada/libgnat/a-coormu.ads
+++ b/gcc/ada/libgnat/a-coormu.ads
@@ -42,7 +42,9 @@ generic
    with function "<" (Left, Right : Element_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Ordered_Multisets is
+package Ada.Containers.Ordered_Multisets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;
diff --git a/gcc/ada/libgnat/a-coorse.adb b/gcc/ada/libgnat/a-coorse.adb
index 8c37d11248a..15b59dd4bc5 100644
--- a/gcc/ada/libgnat/a-coorse.adb
+++ b/gcc/ada/libgnat/a-coorse.adb
@@ -42,7 +42,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Set_Operations);
 
 with System; use type System.Address;
 
-package body Ada.Containers.Ordered_Sets is
+package body Ada.Containers.Ordered_Sets with
+  SPARK_Mode => Off
+is
 
    pragma Warnings (Off, "variable ""Busy*"" is not referenced");
    pragma Warnings (Off, "variable ""Lock*"" is not referenced");
diff --git a/gcc/ada/libgnat/a-coorse.ads b/gcc/ada/libgnat/a-coorse.ads
index 3699e703e1b..42e5b4970f0 100644
--- a/gcc/ada/libgnat/a-coorse.ads
+++ b/gcc/ada/libgnat/a-coorse.ads
@@ -44,7 +44,9 @@ generic
    with function "<" (Left, Right : Element_Type) return Boolean is <>;
    with function "=" (Left, Right : Element_Type) return Boolean is <>;
 
-package Ada.Containers.Ordered_Sets is
+package Ada.Containers.Ordered_Sets with
+  SPARK_Mode => Off
+is
    pragma Annotate (CodePeer, Skip_Analysis);
    pragma Preelaborate;
    pragma Remote_Types;

More information about the Gcc-cvs mailing list