diff options
| author | Yannick Moy <moy@adacore.com> | 2020-06-02 14:16:25 +0200 |
|---|---|---|
| committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2020-07-15 09:42:46 -0400 |
| commit | 3221be144431dae561be518c1411849fa65ac486 (patch) | |
| tree | 92d0235221e5fb68cec2374fd525db681676c60e /gcc/ada/libgnat/a-coorma.adb | |
| parent | bdeeeaf71f1f4a9911d85c5aa5ad0500086201dc (diff) | |
| download | gcc-3221be144431dae561be518c1411849fa65ac486.zip gcc-3221be144431dae561be518c1411849fa65ac486.tar.gz gcc-3221be144431dae561be518c1411849fa65ac486.tar.bz2 | |
[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.
Diffstat (limited to 'gcc/ada/libgnat/a-coorma.adb')
| -rw-r--r-- | gcc/ada/libgnat/a-coorma.adb | 4 |
1 files changed, 3 insertions, 1 deletions
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"); |