From 38818659c388491abe7ab11f8757c1ad2acd1506 Mon Sep 17 00:00:00 2001 From: Joffrey Huguet Date: Thu, 4 Jul 2019 08:07:09 +0000 Subject: [PATCH] [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 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 | 6 ++++++ gcc/ada/libgnarl/a-taside.ads | 9 +++++++++ 2 files changed, 15 insertions(+) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 602bef5..cc88f7f 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,9 @@ +2019-07-04 Joffrey Huguet + + * libgnarl/a-taside.ads: Add assertion policy to ignore + preconditions. + (Abort_Task, Is_Terminated, Is_Callable): Add preconditions. + 2019-07-04 Eric Botcazou * doc/gnat_rm/implementation_defined_pragmas.rst: Fix 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); -- 2.7.4