projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9411732) | patch
[Ada] Mark generic body outside of SPARK
authorYannick Moy <moy@adacore.com>
Fri, 27 Nov 2020 09:13:23 +0000 (10:13 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 16 Dec 2020 13:01:00 +0000 (08:01 -0500)
commitc507c83b324582dc05db91d332b0de4b25c85c07
tree0fa15185b35a4bc6107b1f3f6f3626bba3760ebctree
parent94117322e68f29677f5a7088fc83f57e824ca8a7commit | diff
[Ada] Mark generic body outside of SPARK

gcc/ada/

* libgnat/a-tifiio.adb: Mark body not in SPARK.
* libgnat/a-tifiio.ads: Mark spec in SPARK.
* libgnat/a-tifiio__128.adb: Mark body not in SPARK.
gcc/ada/libgnat/a-tifiio.adb diff | blob | history
gcc/ada/libgnat/a-tifiio.ads diff | blob | history
gcc/ada/libgnat/a-tifiio__128.adb diff | blob | history