From: Yannick Moy Date: Tue, 2 Jun 2020 12:16:25 +0000 (+0200) Subject: [Ada] Mark standard containers as not in SPARK X-Git-Tag: basepoints/gcc-12~6137 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=3221be144431dae561be518c1411849fa65ac486;p=thirdparty%2Fgcc.git [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 1b3a88cd60e1..0f0c872e8878 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 0103a03e688c..74639cf07d29 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 b76bd623cd78..1881db212bcd 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 cf76fbb25e2e..86fed4e69975 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 8a786f1f68e2..a332bd74a7fd 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 663dcb3eaf5c..01903c74a0cd 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 f9048b09c2f3..58db8cf4471d 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 8008e1dcf58e..653407bfcdc6 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 1e384d777e06..6f59471cb7c2 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 1cfc41229ed1..c199a09efbf9 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 af5efc1f5ca7..af4f87f157d5 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 a119c821e444..52b8786f3c8c 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 27b5bd3e829f..2e972912548c 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 e5a9b66b436b..6259a472a722 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 62cad5de8f6d..abb0e7940bad 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 07fe84b33889..61504fa33e72 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 73c7980a157a..a668db11bb13 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 424a346c0df2..89216e03226b 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 a086935dd3a6..0898db8c4014 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 1111bbbb1dc1..e9220a6e257c 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 7c4d427ca247..9f5aed7b02be 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 4d9233a1d7e7..fb6f4e009904 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 3d5af6a17690..b91532dc9741 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 e6dcef69b60b..926e07f1faa1 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 ac7e534380ae..293275ae5a99 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 5d213250ff0c..474a1b57aa96 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 25cf67445f1e..86cd01f09c8b 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 bc4581dd513b..a7799a613a6f 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 62993388a43b..110d734db591 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 ad4e1b247ee9..474ccc75e0d3 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 f9647a2cf400..772061d886c2 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 26cda02a5bf3..1eb8135ff5cf 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 f5424623cf74..7f2d8e16ab53 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 3cc923971df2..9d927bd992b4 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 45a1b2e02941..bc4e53f68f31 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 523e55468d07..3645ed071241 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 85c30fa18325..79e36aea659b 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 2d5443892f7d..075a1843319a 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 6468839e2944..76ff75156162 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 89e57978212e..46934a113c04 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 197271b87c7d..c4d1406383ea 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 8ad31a2ec095..7b2e1760834f 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 9bad901259ae..4106d58ff4ed 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 02d97e416b55..e2d5e1e3e09b 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 66cc77ed3763..c02a9f1540e6 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 cdaee8526ed9..9c6c3ae8d982 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 8c37d11248a9..15b59dd4bc55 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 3699e703e1bc..42e5b4970f08 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;