projects / gcc.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2beb544) | patch
[Ada] Add preconditions in Ada.Task_Identification
authorJoffrey Huguet <huguet@adacore.com>
Thu, 4 Jul 2019 08:07:09 +0000 (08:07 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 4 Jul 2019 08:07:09 +0000 (08:07 +0000)
commit38818659c388491abe7ab11f8757c1ad2acd1506
treeebe22da24bd42a43b98bbf12bb94509fe0d3ce1ctree
parent2beb5444be68bc9b1e580947c133bf3b7e26b8d1commit | diff
[Ada] Add preconditions in Ada.Task_Identification

This patch is needed to check for the Ada RM C.7.1(15) rule in SPARK.

2019-07-04  Joffrey Huguet  <huguet@adacore.com>

gcc/ada/

* libgnarl/a-taside.ads: Add assertion policy to ignore
preconditions.
(Abort_Task, Is_Terminated, Is_Callable): Add preconditions.

From-SVN: r273069
gcc/ada/ChangeLog diff | blob | history
gcc/ada/libgnarl/a-taside.ads diff | blob | history