diff options
Diffstat (limited to 'gcc/ada/libgnat')
48 files changed, 144 insertions, 48 deletions
diff --git a/gcc/ada/libgnat/a-cbdlli.adb b/gcc/ada/libgnat/a-cbdlli.adb index 1b3a88c..0f0c872 100644 --- a/gcc/ada/libgnat/a-cbdlli.adb +++ b/gcc/ada/libgnat/a-cbdlli.adb @@ -29,7 +29,9 @@ with System; use type System.Address; -package body Ada.Containers.Bounded_Doubly_Linked_Lists is +package body Ada.Containers.Bounded_Doubly_Linked_Lists with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cbdlli.ads b/gcc/ada/libgnat/a-cbdlli.ads index 0103a03..74639cf 100644 --- a/gcc/ada/libgnat/a-cbdlli.ads +++ b/gcc/ada/libgnat/a-cbdlli.ads @@ -43,7 +43,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Bounded_Doubly_Linked_Lists is +package Ada.Containers.Bounded_Doubly_Linked_Lists with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Pure; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cbhama.adb b/gcc/ada/libgnat/a-cbhama.adb index b76bd62..1881db2 100644 --- a/gcc/ada/libgnat/a-cbhama.adb +++ b/gcc/ada/libgnat/a-cbhama.adb @@ -39,7 +39,9 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers; with System; use type System.Address; -package body Ada.Containers.Bounded_Hashed_Maps is +package body Ada.Containers.Bounded_Hashed_Maps with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cbhama.ads b/gcc/ada/libgnat/a-cbhama.ads index cf76fbb..86fed4e 100644 --- a/gcc/ada/libgnat/a-cbhama.ads +++ b/gcc/ada/libgnat/a-cbhama.ads @@ -45,7 +45,9 @@ generic with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Bounded_Hashed_Maps is +package Ada.Containers.Bounded_Hashed_Maps with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Pure; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cbhase.adb b/gcc/ada/libgnat/a-cbhase.adb index 8a786f1..a332bd7 100644 --- a/gcc/ada/libgnat/a-cbhase.adb +++ b/gcc/ada/libgnat/a-cbhase.adb @@ -39,7 +39,9 @@ with Ada.Containers.Prime_Numbers; use Ada.Containers.Prime_Numbers; with System; use type System.Address; -package body Ada.Containers.Bounded_Hashed_Sets is +package body Ada.Containers.Bounded_Hashed_Sets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cbhase.ads b/gcc/ada/libgnat/a-cbhase.ads index 663dcb3..01903c7 100644 --- a/gcc/ada/libgnat/a-cbhase.ads +++ b/gcc/ada/libgnat/a-cbhase.ads @@ -48,7 +48,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Bounded_Hashed_Sets is +package Ada.Containers.Bounded_Hashed_Sets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Pure; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cbmutr.adb b/gcc/ada/libgnat/a-cbmutr.adb index f9048b0..58db8cf 100644 --- a/gcc/ada/libgnat/a-cbmutr.adb +++ b/gcc/ada/libgnat/a-cbmutr.adb @@ -30,7 +30,9 @@ with Ada.Finalization; with System; use type System.Address; -package body Ada.Containers.Bounded_Multiway_Trees is +package body Ada.Containers.Bounded_Multiway_Trees with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cbmutr.ads b/gcc/ada/libgnat/a-cbmutr.ads index 8008e1d..653407b 100644 --- a/gcc/ada/libgnat/a-cbmutr.ads +++ b/gcc/ada/libgnat/a-cbmutr.ads @@ -41,7 +41,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Bounded_Multiway_Trees is +package Ada.Containers.Bounded_Multiway_Trees with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Pure; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cborma.adb b/gcc/ada/libgnat/a-cborma.adb index 1e384d7..6f59471 100644 --- a/gcc/ada/libgnat/a-cborma.adb +++ b/gcc/ada/libgnat/a-cborma.adb @@ -39,7 +39,9 @@ pragma Elaborate_All with System; use type System.Address; -package body Ada.Containers.Bounded_Ordered_Maps is +package body Ada.Containers.Bounded_Ordered_Maps with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cborma.ads b/gcc/ada/libgnat/a-cborma.ads index 1cfc412..c199a09 100644 --- a/gcc/ada/libgnat/a-cborma.ads +++ b/gcc/ada/libgnat/a-cborma.ads @@ -44,7 +44,9 @@ generic with function "<" (Left, Right : Key_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Bounded_Ordered_Maps is +package Ada.Containers.Bounded_Ordered_Maps with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Pure; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cborse.adb b/gcc/ada/libgnat/a-cborse.adb index af5efc1..af4f87f 100644 --- a/gcc/ada/libgnat/a-cborse.adb +++ b/gcc/ada/libgnat/a-cborse.adb @@ -42,7 +42,9 @@ pragma Elaborate_All with System; use type System.Address; -package body Ada.Containers.Bounded_Ordered_Sets is +package body Ada.Containers.Bounded_Ordered_Sets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cborse.ads b/gcc/ada/libgnat/a-cborse.ads index a119c82..52b8786 100644 --- a/gcc/ada/libgnat/a-cborse.ads +++ b/gcc/ada/libgnat/a-cborse.ads @@ -44,7 +44,9 @@ generic with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Bounded_Ordered_Sets is +package Ada.Containers.Bounded_Ordered_Sets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Pure; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cbprqu.adb b/gcc/ada/libgnat/a-cbprqu.adb index 27b5bd3..2e97291 100644 --- a/gcc/ada/libgnat/a-cbprqu.adb +++ b/gcc/ada/libgnat/a-cbprqu.adb @@ -27,7 +27,9 @@ -- This unit was originally developed by Matthew J Heaney. -- ------------------------------------------------------------------------------ -package body Ada.Containers.Bounded_Priority_Queues is +package body Ada.Containers.Bounded_Priority_Queues with + SPARK_Mode => Off +is package body Implementation is diff --git a/gcc/ada/libgnat/a-cbprqu.ads b/gcc/ada/libgnat/a-cbprqu.ads index e5a9b66..6259a47 100644 --- a/gcc/ada/libgnat/a-cbprqu.ads +++ b/gcc/ada/libgnat/a-cbprqu.ads @@ -51,7 +51,9 @@ generic Default_Capacity : Count_Type; Default_Ceiling : System.Any_Priority := System.Priority'Last; -package Ada.Containers.Bounded_Priority_Queues is +package Ada.Containers.Bounded_Priority_Queues with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; diff --git a/gcc/ada/libgnat/a-cbsyqu.adb b/gcc/ada/libgnat/a-cbsyqu.adb index 62cad5d..abb0e79 100644 --- a/gcc/ada/libgnat/a-cbsyqu.adb +++ b/gcc/ada/libgnat/a-cbsyqu.adb @@ -27,7 +27,9 @@ -- This unit was originally developed by Matthew J Heaney. -- ------------------------------------------------------------------------------ -package body Ada.Containers.Bounded_Synchronized_Queues is +package body Ada.Containers.Bounded_Synchronized_Queues with + SPARK_Mode => Off +is package body Implementation is diff --git a/gcc/ada/libgnat/a-cbsyqu.ads b/gcc/ada/libgnat/a-cbsyqu.ads index 07fe84b..61504fa 100644 --- a/gcc/ada/libgnat/a-cbsyqu.ads +++ b/gcc/ada/libgnat/a-cbsyqu.ads @@ -41,7 +41,9 @@ generic Default_Capacity : Count_Type; Default_Ceiling : System.Any_Priority := System.Priority'Last; -package Ada.Containers.Bounded_Synchronized_Queues is +package Ada.Containers.Bounded_Synchronized_Queues with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; diff --git a/gcc/ada/libgnat/a-cdlili.adb b/gcc/ada/libgnat/a-cdlili.adb index 73c7980..a668db1 100644 --- a/gcc/ada/libgnat/a-cdlili.adb +++ b/gcc/ada/libgnat/a-cdlili.adb @@ -31,7 +31,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Doubly_Linked_Lists is +package body Ada.Containers.Doubly_Linked_Lists with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cdlili.ads b/gcc/ada/libgnat/a-cdlili.ads index 424a346..89216e0 100644 --- a/gcc/ada/libgnat/a-cdlili.ads +++ b/gcc/ada/libgnat/a-cdlili.ads @@ -43,7 +43,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Doubly_Linked_Lists is +package Ada.Containers.Doubly_Linked_Lists with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cidlli.adb b/gcc/ada/libgnat/a-cidlli.adb index a086935..0898db8 100644 --- a/gcc/ada/libgnat/a-cidlli.adb +++ b/gcc/ada/libgnat/a-cidlli.adb @@ -31,7 +31,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Indefinite_Doubly_Linked_Lists is +package body Ada.Containers.Indefinite_Doubly_Linked_Lists with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cidlli.ads b/gcc/ada/libgnat/a-cidlli.ads index 1111bbb..e9220a6 100644 --- a/gcc/ada/libgnat/a-cidlli.ads +++ b/gcc/ada/libgnat/a-cidlli.ads @@ -43,7 +43,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Doubly_Linked_Lists is +package Ada.Containers.Indefinite_Doubly_Linked_Lists with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cihama.adb b/gcc/ada/libgnat/a-cihama.adb index 7c4d427c..9f5aed7 100644 --- a/gcc/ada/libgnat/a-cihama.adb +++ b/gcc/ada/libgnat/a-cihama.adb @@ -39,7 +39,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Indefinite_Hashed_Maps is +package body Ada.Containers.Indefinite_Hashed_Maps with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cihama.ads b/gcc/ada/libgnat/a-cihama.ads index 4d9233a..fb6f4e0 100644 --- a/gcc/ada/libgnat/a-cihama.ads +++ b/gcc/ada/libgnat/a-cihama.ads @@ -45,7 +45,9 @@ generic with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Hashed_Maps is +package Ada.Containers.Indefinite_Hashed_Maps with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cihase.adb b/gcc/ada/libgnat/a-cihase.adb index 3d5af6a..b91532d 100644 --- a/gcc/ada/libgnat/a-cihase.adb +++ b/gcc/ada/libgnat/a-cihase.adb @@ -41,7 +41,9 @@ with Ada.Containers.Prime_Numbers; with System; use type System.Address; -package body Ada.Containers.Indefinite_Hashed_Sets is +package body Ada.Containers.Indefinite_Hashed_Sets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cihase.ads b/gcc/ada/libgnat/a-cihase.ads index e6dcef6..926e07f 100644 --- a/gcc/ada/libgnat/a-cihase.ads +++ b/gcc/ada/libgnat/a-cihase.ads @@ -48,7 +48,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Hashed_Sets is +package Ada.Containers.Indefinite_Hashed_Sets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cimutr.adb b/gcc/ada/libgnat/a-cimutr.adb index ac7e534..293275a 100644 --- a/gcc/ada/libgnat/a-cimutr.adb +++ b/gcc/ada/libgnat/a-cimutr.adb @@ -31,7 +31,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Indefinite_Multiway_Trees is +package body Ada.Containers.Indefinite_Multiway_Trees with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cimutr.ads b/gcc/ada/libgnat/a-cimutr.ads index 5d21325..474a1b5 100644 --- a/gcc/ada/libgnat/a-cimutr.ads +++ b/gcc/ada/libgnat/a-cimutr.ads @@ -42,7 +42,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Multiway_Trees is +package Ada.Containers.Indefinite_Multiway_Trees with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-ciorma.adb b/gcc/ada/libgnat/a-ciorma.adb index 25cf674..86cd01f 100644 --- a/gcc/ada/libgnat/a-ciorma.adb +++ b/gcc/ada/libgnat/a-ciorma.adb @@ -39,7 +39,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Keys); with System; use type System.Address; -package body Ada.Containers.Indefinite_Ordered_Maps is +package body Ada.Containers.Indefinite_Ordered_Maps with + SPARK_Mode => Off +is pragma Suppress (All_Checks); pragma Warnings (Off, "variable ""Busy*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-ciorma.ads b/gcc/ada/libgnat/a-ciorma.ads index bc4581d..a7799a6 100644 --- a/gcc/ada/libgnat/a-ciorma.ads +++ b/gcc/ada/libgnat/a-ciorma.ads @@ -44,7 +44,9 @@ generic with function "<" (Left, Right : Key_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Ordered_Maps is +package Ada.Containers.Indefinite_Ordered_Maps with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-ciormu.adb b/gcc/ada/libgnat/a-ciormu.adb index 6299338..110d734 100644 --- a/gcc/ada/libgnat/a-ciormu.adb +++ b/gcc/ada/libgnat/a-ciormu.adb @@ -40,7 +40,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Set_Operations); with System; use type System.Address; -package body Ada.Containers.Indefinite_Ordered_Multisets is +package body Ada.Containers.Indefinite_Ordered_Multisets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-ciormu.ads b/gcc/ada/libgnat/a-ciormu.ads index ad4e1b2..474ccc7 100644 --- a/gcc/ada/libgnat/a-ciormu.ads +++ b/gcc/ada/libgnat/a-ciormu.ads @@ -43,7 +43,9 @@ generic with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Ordered_Multisets is +package Ada.Containers.Indefinite_Ordered_Multisets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-ciorse.adb b/gcc/ada/libgnat/a-ciorse.adb index f9647a2..772061d 100644 --- a/gcc/ada/libgnat/a-ciorse.adb +++ b/gcc/ada/libgnat/a-ciorse.adb @@ -42,7 +42,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Indefinite_Ordered_Sets is +package body Ada.Containers.Indefinite_Ordered_Sets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-ciorse.ads b/gcc/ada/libgnat/a-ciorse.ads index 26cda02..1eb8135 100644 --- a/gcc/ada/libgnat/a-ciorse.ads +++ b/gcc/ada/libgnat/a-ciorse.ads @@ -44,7 +44,9 @@ generic with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Ordered_Sets is +package Ada.Containers.Indefinite_Ordered_Sets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cohama.adb b/gcc/ada/libgnat/a-cohama.adb index f542462..7f2d8e1 100644 --- a/gcc/ada/libgnat/a-cohama.adb +++ b/gcc/ada/libgnat/a-cohama.adb @@ -39,7 +39,9 @@ with Ada.Containers.Helpers; use Ada.Containers.Helpers; with System; use type System.Address; -package body Ada.Containers.Hashed_Maps is +package body Ada.Containers.Hashed_Maps with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cohama.ads b/gcc/ada/libgnat/a-cohama.ads index 3cc9239..9d927bd 100644 --- a/gcc/ada/libgnat/a-cohama.ads +++ b/gcc/ada/libgnat/a-cohama.ads @@ -88,7 +88,9 @@ generic -- map values returns an unspecified value. The exact arguments and number -- of calls of this generic formal function by the function "=" on map -- values are unspecified. -package Ada.Containers.Hashed_Maps is +package Ada.Containers.Hashed_Maps with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-cohase.adb b/gcc/ada/libgnat/a-cohase.adb index 45a1b2e..bc4e53f 100644 --- a/gcc/ada/libgnat/a-cohase.adb +++ b/gcc/ada/libgnat/a-cohase.adb @@ -41,7 +41,9 @@ with Ada.Containers.Prime_Numbers; with System; use type System.Address; -package body Ada.Containers.Hashed_Sets is +package body Ada.Containers.Hashed_Sets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-cohase.ads b/gcc/ada/libgnat/a-cohase.ads index 523e554..3645ed0 100644 --- a/gcc/ada/libgnat/a-cohase.ads +++ b/gcc/ada/libgnat/a-cohase.ads @@ -48,7 +48,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Hashed_Sets is +package Ada.Containers.Hashed_Sets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-coinve.adb b/gcc/ada/libgnat/a-coinve.adb index 85c30fa..79e36ae 100644 --- a/gcc/ada/libgnat/a-coinve.adb +++ b/gcc/ada/libgnat/a-coinve.adb @@ -32,7 +32,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Indefinite_Vectors is +package body Ada.Containers.Indefinite_Vectors with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-coinve.ads b/gcc/ada/libgnat/a-coinve.ads index 2d54438..075a184 100644 --- a/gcc/ada/libgnat/a-coinve.ads +++ b/gcc/ada/libgnat/a-coinve.ads @@ -43,7 +43,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Indefinite_Vectors is +package Ada.Containers.Indefinite_Vectors with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-comutr.adb b/gcc/ada/libgnat/a-comutr.adb index 6468839..76ff751 100644 --- a/gcc/ada/libgnat/a-comutr.adb +++ b/gcc/ada/libgnat/a-comutr.adb @@ -32,7 +32,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Multiway_Trees is +package body Ada.Containers.Multiway_Trees with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-comutr.ads b/gcc/ada/libgnat/a-comutr.ads index 89e5797..46934a1 100644 --- a/gcc/ada/libgnat/a-comutr.ads +++ b/gcc/ada/libgnat/a-comutr.ads @@ -42,7 +42,9 @@ generic with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Multiway_Trees is +package Ada.Containers.Multiway_Trees with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-convec.adb b/gcc/ada/libgnat/a-convec.adb index 197271b..c4d1406 100644 --- a/gcc/ada/libgnat/a-convec.adb +++ b/gcc/ada/libgnat/a-convec.adb @@ -32,7 +32,9 @@ with Ada.Unchecked_Deallocation; with System; use type System.Address; -package body Ada.Containers.Vectors is +package body Ada.Containers.Vectors with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-convec.ads b/gcc/ada/libgnat/a-convec.ads index 8ad31a2..7b2e176 100644 --- a/gcc/ada/libgnat/a-convec.ads +++ b/gcc/ada/libgnat/a-convec.ads @@ -70,7 +70,9 @@ generic -- number of calls of this generic formal function by the functions defined -- to use it are unspecified. -package Ada.Containers.Vectors is +package Ada.Containers.Vectors with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-coorma.adb b/gcc/ada/libgnat/a-coorma.adb index 9bad901..4106d58 100644 --- a/gcc/ada/libgnat/a-coorma.adb +++ b/gcc/ada/libgnat/a-coorma.adb @@ -39,7 +39,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Keys); with System; use type System.Address; -package body Ada.Containers.Ordered_Maps is +package body Ada.Containers.Ordered_Maps with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-coorma.ads b/gcc/ada/libgnat/a-coorma.ads index 02d97e4..e2d5e1e 100644 --- a/gcc/ada/libgnat/a-coorma.ads +++ b/gcc/ada/libgnat/a-coorma.ads @@ -44,7 +44,9 @@ generic with function "<" (Left, Right : Key_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Ordered_Maps is +package Ada.Containers.Ordered_Maps with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-coormu.adb b/gcc/ada/libgnat/a-coormu.adb index 66cc77e..c02a9f1 100644 --- a/gcc/ada/libgnat/a-coormu.adb +++ b/gcc/ada/libgnat/a-coormu.adb @@ -40,7 +40,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Set_Operations); with System; use type System.Address; -package body Ada.Containers.Ordered_Multisets is +package body Ada.Containers.Ordered_Multisets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-coormu.ads b/gcc/ada/libgnat/a-coormu.ads index cdaee85..9c6c3ae 100644 --- a/gcc/ada/libgnat/a-coormu.ads +++ b/gcc/ada/libgnat/a-coormu.ads @@ -42,7 +42,9 @@ generic with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Ordered_Multisets is +package Ada.Containers.Ordered_Multisets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; diff --git a/gcc/ada/libgnat/a-coorse.adb b/gcc/ada/libgnat/a-coorse.adb index 8c37d11..15b59dd 100644 --- a/gcc/ada/libgnat/a-coorse.adb +++ b/gcc/ada/libgnat/a-coorse.adb @@ -42,7 +42,9 @@ pragma Elaborate_All (Ada.Containers.Red_Black_Trees.Generic_Set_Operations); with System; use type System.Address; -package body Ada.Containers.Ordered_Sets is +package body Ada.Containers.Ordered_Sets with + SPARK_Mode => Off +is pragma Warnings (Off, "variable ""Busy*"" is not referenced"); pragma Warnings (Off, "variable ""Lock*"" is not referenced"); diff --git a/gcc/ada/libgnat/a-coorse.ads b/gcc/ada/libgnat/a-coorse.ads index 3699e70..42e5b49 100644 --- a/gcc/ada/libgnat/a-coorse.ads +++ b/gcc/ada/libgnat/a-coorse.ads @@ -44,7 +44,9 @@ generic with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Ordered_Sets is +package Ada.Containers.Ordered_Sets with + SPARK_Mode => Off +is pragma Annotate (CodePeer, Skip_Analysis); pragma Preelaborate; pragma Remote_Types; |