[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.

48 files changed, 144 insertions, 48 deletions

diff --git a/gcc/ada/libgnat/a-cbdlli.adb b/gcc/ada/libgnat/a-cbdlli.adb
index 1b3a88c..0f0c872 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 0103a03..74639cf 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 b76bd62..1881db2 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 cf76fbb..86fed4e 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 8a786f1..a332bd7 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 663dcb3..01903c7 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 f9048b0..58db8cf 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 8008e1d..653407b 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 1e384d7..6f59471 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 1cfc412..c199a09 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 af5efc1..af4f87f 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 a119c82..52b8786 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 27b5bd3..2e97291 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 e5a9b66..6259a47 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 62cad5d..abb0e79 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 07fe84b..61504fa 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 73c7980..a668db1 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 424a346..89216e0 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 a086935..0898db8 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 1111bbb..e9220a6 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 7c4d427c..9f5aed7 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 4d9233a..fb6f4e0 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 3d5af6a..b91532d 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 e6dcef6..926e07f 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 ac7e534..293275a 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 5d21325..474a1b5 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 25cf674..86cd01f 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 bc4581d..a7799a6 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 6299338..110d734 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 ad4e1b2..474ccc7 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 f9647a2..772061d 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 26cda02..1eb8135 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 f542462..7f2d8e1 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 3cc9239..9d927bd 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 45a1b2e..bc4e53f 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 523e554..3645ed0 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 85c30fa..79e36ae 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 2d54438..075a184 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 6468839..76ff751 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 89e5797..46934a1 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 197271b..c4d1406 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 8ad31a2..7b2e176 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 9bad901..4106d58 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 02d97e4..e2d5e1e 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 66cc77e..c02a9f1 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 cdaee85..9c6c3ae 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 8c37d11..15b59dd 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 3699e70..42e5b49 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;