[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 --git a/gcc/ada/libgnat/a-cbdlli.adb b/gcc/ada/libgnat/a-cbdlli.adb
index 1b3a88cd60e1b3f129c7f7345f296f2a84fceaed..0f0c872e8878226928c8bc3da19c4bfa9ac325eb 100644 (file)
--- 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 0103a03e688c7b0acb18840cfc21b69a0185f57d..74639cf07d295746b3c4b3b7650b4f96cf3b48c1 100644 (file)
--- 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 b76bd623cd78234ef8472f6da63a2884fea53165..1881db212bcd0e52c96d51461b30111eef385e06 100644 (file)
--- 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 cf76fbb25e2ed5977f2d94421b8cdfde27740251..86fed4e699758effa9ca9ebfb90a2467de2b58d8 100644 (file)
--- 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 8a786f1f68e260f743e0208bc53b4f3861f069e7..a332bd74a7fd6657a245f336f685016642082660 100644 (file)
--- 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 663dcb3eaf5cfdbbbbb7a6255e97f8a179217bfb..01903c74a0cd05bc75766f312107ada6e8598059 100644 (file)
--- 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 f9048b09c2f319f866a8d721b82bab409f4aefc0..58db8cf4471d0e9bd044d6494f4a4db953d6041e 100644 (file)
--- 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 8008e1dcf58e4e0b1065fa0a7d281d1a3ec88cb8..653407bfcdc60507f98320470155613635271d64 100644 (file)
--- 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 1e384d777e066ff0e9c1d8e56e6276b749f95df5..6f59471cb7c2a06b33cfe6bd1a26e4c96b9874df 100644 (file)
--- 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 1cfc41229ed1514ba26f288c24c8ccfb94ed53b3..c199a09efbf99a1deb59d6273eb1b675f4b74ca2 100644 (file)
--- 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 af5efc1f5ca705d03a1a7d077f9566754a63e75f..af4f87f157d58538899f0d086097a0f9b0bab193 100644 (file)
--- 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 a119c821e444dcad81d13766695528a71dd07517..52b8786f3c8c89c2e75622ddcbd23d783c7b969c 100644 (file)
--- 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 27b5bd3e829f833b9b19caa8d67f3e9811648793..2e972912548c0d6a9f0c6047c52523e52009244a 100644 (file)
--- 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 e5a9b66b436b58a234d6fb2968629167ac08cd8a..6259a472a72246927a3728eaafe1c5503f86460f 100644 (file)
--- 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 62cad5de8f6d1861f2533a3abbcacb926ce430f9..abb0e7940bad6dabc25df7c2fbaf07808786a98d 100644 (file)
--- 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 07fe84b3388956a2617da3760f7406f8af6ff242..61504fa33e72bd30645af463c2137b39f556eea9 100644 (file)
--- 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 73c7980a157a9ffe7cde9a04cc68eb45dd9aa5ea..a668db11bb132c719d75fb699d306c5d86b9b994 100644 (file)
--- 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 424a346c0df256602caad789b71d1b8c0f37e809..89216e03226b97bf56a963bdab3fedc5d040eae5 100644 (file)
--- 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 a086935dd3a6d3b9262e21115ee492b80b234be5..0898db8c401444d6d6408c5fe00b8bb8bf581004 100644 (file)
--- 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 1111bbbb1dc10fb39e1d53df076539fa90247eb9..e9220a6e257cd7e3bd2efcbd9c4417d28fd80772 100644 (file)
--- 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 7c4d427ca2475fa86b5db63d9f4e032a3fc4cbcc..9f5aed7b02be81c70394df051ee9178979928fa8 100644 (file)
--- 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 4d9233a1d7e70ca46dbf9238ab6fda64b2b233c3..fb6f4e009904211984673631cc0590c98ddb0e6e 100644 (file)
--- 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 3d5af6a1769016ae1f77c59506b651722c17f517..b91532dc9741e866148b020a415d616e88e35c5d 100644 (file)
--- 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 e6dcef69b60b238933ded53131471f8f78e4d344..926e07f1faa11f19f5d2ded68739e2bd0c983e2b 100644 (file)
--- 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 ac7e534380ae40b30b066db481c8c85e07fbc2bf..293275ae5a99c1d7bcbccb39461eb013098efcc3 100644 (file)
--- 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 5d213250ff0c7ceb3d57448eb63e82a4e0bbf338..474a1b57aa96207adaba23c43773e3314987f9f1 100644 (file)
--- 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 25cf67445f1ec607b0ffea057ec11aa935745a05..86cd01f09c8b00b7ecb2ef57a34fd27d17eb3ea5 100644 (file)
--- 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 bc4581dd513b97b0ed463dfc96a21ee9fd0d7eaa..a7799a613a6f944847f325d6d16c1e2bac39c182 100644 (file)
--- 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 62993388a43b74bd78b0346b9adbadfb3f0fbc21..110d734db5914047919a3fee4fcc02253aa6e559 100644 (file)
--- 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 ad4e1b247ee913ca0553148609fae86ca163b754..474ccc75e0d3595b366aa277c5a3dbb312bad7aa 100644 (file)
--- 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 f9647a2cf400d2a3a2c063371fef3aaeb13f4ce3..772061d886c22123f3441c778ab0351560d40301 100644 (file)
--- 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 26cda02a5bf3e2703f1052ee1c4bbe0f6216b390..1eb8135ff5cf2e4e5522a2f11ce2c112d1e76313 100644 (file)
--- 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 f5424623cf74a9a32458c32d31ac564949a9a54d..7f2d8e16ab5361661eafa5d1f9dca33ca5cbb735 100644 (file)
--- 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 3cc923971df242f4a037ccd7f2a378d2523104b4..9d927bd992b437ffc0fd95e54c5e5e1fa0ef47fd 100644 (file)
--- 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 45a1b2e029412a207dba9f377a75245328777508..bc4e53f68f3108a836694eb8fee35b080a6c4260 100644 (file)
--- 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 523e55468d0708708f220eb42db55f3a2ab8f1ba..3645ed071241b9e29497898dcdf24c6b35d512db 100644 (file)
--- 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 85c30fa1832529dc94592c2bec3fa7c107cbec47..79e36aea659b0d11e68783d5a4247f2a0fd568b2 100644 (file)
--- 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 2d5443892f7dca4e7c0fc70b3b0c44c26f8347e4..075a1843319a7fe76ecd14970cac528e5e8be416 100644 (file)
--- 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 6468839e294409a3419db33ae475ec5b7b02a70e..76ff751561621a9e9654623707ef4f83843e42f9 100644 (file)
--- 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 89e57978212e880f219c4c721fa8f913f6367917..46934a113c04ab05c9fba3ab69efa55bb2fcc7c6 100644 (file)
--- 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 197271b87c7daa0423a8328456467d7ca5b315b7..c4d1406383ea4707c65dd830b10071294825235e 100644 (file)
--- 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 8ad31a2ec095acae7be47ccd5ac253a1c3be077c..7b2e1760834f0345b843c4a2efc4a36f8f005036 100644 (file)
--- 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 9bad901259aeddb42f147f124189401b45cdbdcd..4106d58ff4ed8b1ae6b9115cb9a21cd69d21c16f 100644 (file)
--- 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 02d97e416b559bda0faa9d8d86484f91a4b0ce74..e2d5e1e3e09b43117ae7fddb1ad60a93fbd45197 100644 (file)
--- 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 66cc77ed3763583cfad408fdc60ba8f08b727cc8..c02a9f1540e666655959cafa78ec34e568bb4deb 100644 (file)
--- 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 cdaee8526ed91a803bbbfcba25f099817b753fd6..9c6c3ae8d982c6075590fdf9e588a73712f6cd80 100644 (file)
--- 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 8c37d11248a9be6d8ecd5f48261b4eb08e19c133..15b59dd4bc55cef271e0c7b0d96042553539a0b9 100644 (file)
--- 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 3699e703e1bce8f111ec15b881d7295ad956ee75..42e5b4970f08f50510681c305fe33be31452af95 100644 (file)
--- 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;