]> git.ipfire.org Git - thirdparty/gcc.git/commit
[Ada] Proof of the runtime support for attribute 'Width
authorYannick Moy <moy@adacore.com>
Mon, 30 Aug 2021 14:33:00 +0000 (16:33 +0200)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 20 Oct 2021 10:17:06 +0000 (10:17 +0000)
commitbd2560b726fa93b61060a9f469ad288c512961f3
tree520d242ef6824d20f9c41d059d56cac53ef42762
parentc5742a0e1191365c57bc06fdbf1ff5da1028f127
[Ada] Proof of the runtime support for attribute 'Width

gcc/ada/

* libgnat/s-widlllu.ads: Mark in SPARK.
* libgnat/s-widllu.ads: Likewise.
* libgnat/s-widuns.ads: Likewise.
* libgnat/s-widthu.adb: Add ghost code and a
pseudo-postcondition.
gcc/ada/libgnat/s-widlllu.ads
gcc/ada/libgnat/s-widllu.ads
gcc/ada/libgnat/s-widthu.adb
gcc/ada/libgnat/s-widuns.ads