diff options
| author | Joffrey Huguet <huguet@adacore.com> | 2019-07-04 08:07:09 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-04 08:07:09 +0000 |
| commit | 38818659c388491abe7ab11f8757c1ad2acd1506 (patch) | |
| tree | ebe22da24bd42a43b98bbf12bb94509fe0d3ce1c /gcc/tree-object-size.c | |
| parent | 2beb5444be68bc9b1e580947c133bf3b7e26b8d1 (diff) | |
| download | gcc-38818659c388491abe7ab11f8757c1ad2acd1506.zip gcc-38818659c388491abe7ab11f8757c1ad2acd1506.tar.gz gcc-38818659c388491abe7ab11f8757c1ad2acd1506.tar.bz2 | |
[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
Diffstat (limited to 'gcc/tree-object-size.c')
0 files changed, 0 insertions, 0 deletions