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/ada/libgnarl | |
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/ada/libgnarl')
-rw-r--r-- | gcc/ada/libgnarl/a-taside.ads | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/gcc/ada/libgnarl/a-taside.ads b/gcc/ada/libgnarl/a-taside.ads index 4939d1e..6bdb252 100644 --- a/gcc/ada/libgnarl/a-taside.ads +++ b/gcc/ada/libgnarl/a-taside.ads @@ -33,6 +33,12 @@ -- -- ------------------------------------------------------------------------------ +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. +-- This is enforced by setting the corresponding assertion policy to Ignore. + +pragma Assertion_Policy (Pre => Ignore); + with System; with System.Tasking; @@ -67,17 +73,20 @@ is pragma Inline (Environment_Task); procedure Abort_Task (T : Task_Id) with + Pre => T /= Null_Task_Id, Global => null; pragma Inline (Abort_Task); -- Note: parameter is mode IN, not IN OUT, per AI-00101 function Is_Terminated (T : Task_Id) return Boolean with Volatile_Function, + Pre => T /= Null_Task_Id, Global => Tasking_State; pragma Inline (Is_Terminated); function Is_Callable (T : Task_Id) return Boolean with Volatile_Function, + Pre => T /= Null_Task_Id, Global => Tasking_State; pragma Inline (Is_Callable); |