aboutsummaryrefslogtreecommitdiff
path: root/gcc
diff options
context:
space:
mode:
authorPiotr Trojanek <trojanek@adacore.com>2021-11-17 14:24:25 +0100
committerPierre-Marie de Rodat <derodat@adacore.com>2021-12-02 16:26:20 +0000
commit7e650bf84bf61e88f05ffbf39ca677a1e3d2714a (patch)
treecbdb80a0a212f2d502dda2b8df2d066dc1823941 /gcc
parent45be7610383af22b552ab7b2d0fa0e1d632c66f0 (diff)
downloadgcc-7e650bf84bf61e88f05ffbf39ca677a1e3d2714a.zip
gcc-7e650bf84bf61e88f05ffbf39ca677a1e3d2714a.tar.gz
gcc-7e650bf84bf61e88f05ffbf39ca677a1e3d2714a.tar.bz2
[Ada] Add contract to Ada.Task_Identification.Activation_Is_Complete
gcc/ada/ * libgnarl/a-taside.ads (Activation_Is_Complete): Add precondition.
Diffstat (limited to 'gcc')
-rw-r--r--gcc/ada/libgnarl/a-taside.ads1
1 files changed, 1 insertions, 0 deletions
diff --git a/gcc/ada/libgnarl/a-taside.ads b/gcc/ada/libgnarl/a-taside.ads
index a3b1e94..682211c 100644
--- a/gcc/ada/libgnarl/a-taside.ads
+++ b/gcc/ada/libgnarl/a-taside.ads
@@ -92,6 +92,7 @@ is
function Activation_Is_Complete (T : Task_Id) return Boolean with
Volatile_Function,
+ Pre => T /= Null_Task_Id,
Global => Tasking_State;
private