Use aspect SPARK_Mode with value Off in the spec and body of standard
containers, bounded and unbounded versions, so that it is clearer that
they cannot be used in SPARK code. Formal containers should be used
instead.
Tested on x86_64-pc-linux-gnu, committed on trunk
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 --git a/gcc/ada/libgnat/a-cbdlli.adb b/gcc/ada/libgnat/a-cbdlli.adb
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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;
