From: Joffrey Huguet <huguet@adacore.com>
Date: Thu, 4 Jul 2019 08:07:09 +0000 (+0000)
Subject: [Ada] Add preconditions in Ada.Task_Identification
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=38818659c388491abe7ab11f8757c1ad2acd1506;p=gcc.git

[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 602bef5d031..cc88f7f8c30 100644
--- 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 4939d1eb01a..6bdb252306b 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);