[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

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 602bef5d031462922354a94bc49cc9ded9e9c196..cc88f7f8c30a0cdef3c80c848594dc9d600f857a 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2019-07-04  Joffrey Huguet  <huguet@adacore.com>
+
+       * libgnarl/a-taside.ads: Add assertion policy to ignore
+       preconditions.
+       (Abort_Task, Is_Terminated, Is_Callable): Add preconditions.
+
 2019-07-04  Eric Botcazou  <ebotcazou@adacore.com>
 
        * 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 4939d1eb01ac399e6ee395d5f9481c2281a1aa68..6bdb252306bd14851af71e8e2d3cd0d54bd2d335 100644 (file)
--- 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);