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-coormu.ads | |
| 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-coormu.ads')
| -rw-r--r-- | gcc/ada/libgnat/a-coormu.ads | 4 |
1 files changed, 3 insertions, 1 deletions
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; |