[Ada] Mark standard containers as not in SPARK
authorYannick Moy <moy@adacore.com>
Tue, 2 Jun 2020 12:16:25 +0000 (14:16 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 15 Jul 2020 13:42:46 +0000 (09:42 -0400)
commit3221be144431dae561be518c1411849fa65ac486
tree92d0235221e5fb68cec2374fd525db681676c60e
parentbdeeeaf71f1f4a9911d85c5aa5ad0500086201dc
[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.
48 files changed:
gcc/ada/libgnat/a-cbdlli.adb
gcc/ada/libgnat/a-cbdlli.ads
gcc/ada/libgnat/a-cbhama.adb
gcc/ada/libgnat/a-cbhama.ads
gcc/ada/libgnat/a-cbhase.adb
gcc/ada/libgnat/a-cbhase.ads
gcc/ada/libgnat/a-cbmutr.adb
gcc/ada/libgnat/a-cbmutr.ads
gcc/ada/libgnat/a-cborma.adb
gcc/ada/libgnat/a-cborma.ads
gcc/ada/libgnat/a-cborse.adb
gcc/ada/libgnat/a-cborse.ads
gcc/ada/libgnat/a-cbprqu.adb
gcc/ada/libgnat/a-cbprqu.ads
gcc/ada/libgnat/a-cbsyqu.adb
gcc/ada/libgnat/a-cbsyqu.ads
gcc/ada/libgnat/a-cdlili.adb
gcc/ada/libgnat/a-cdlili.ads
gcc/ada/libgnat/a-cidlli.adb
gcc/ada/libgnat/a-cidlli.ads
gcc/ada/libgnat/a-cihama.adb
gcc/ada/libgnat/a-cihama.ads
gcc/ada/libgnat/a-cihase.adb
gcc/ada/libgnat/a-cihase.ads
gcc/ada/libgnat/a-cimutr.adb
gcc/ada/libgnat/a-cimutr.ads
gcc/ada/libgnat/a-ciorma.adb
gcc/ada/libgnat/a-ciorma.ads
gcc/ada/libgnat/a-ciormu.adb
gcc/ada/libgnat/a-ciormu.ads
gcc/ada/libgnat/a-ciorse.adb
gcc/ada/libgnat/a-ciorse.ads
gcc/ada/libgnat/a-cohama.adb
gcc/ada/libgnat/a-cohama.ads
gcc/ada/libgnat/a-cohase.adb
gcc/ada/libgnat/a-cohase.ads
gcc/ada/libgnat/a-coinve.adb
gcc/ada/libgnat/a-coinve.ads
gcc/ada/libgnat/a-comutr.adb
gcc/ada/libgnat/a-comutr.ads
gcc/ada/libgnat/a-convec.adb
gcc/ada/libgnat/a-convec.ads
gcc/ada/libgnat/a-coorma.adb
gcc/ada/libgnat/a-coorma.ads
gcc/ada/libgnat/a-coormu.adb
gcc/ada/libgnat/a-coormu.ads
gcc/ada/libgnat/a-coorse.adb
gcc/ada/libgnat/a-coorse.ads