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