diff mbox series

[Ada] Add contract to Ada.Task_Identification.Activation_Is_Complete

Message ID 20211202162837.GA2156244@adacore.com
State New
Headers show
Series [Ada] Add contract to Ada.Task_Identification.Activation_Is_Complete | expand

Commit Message

Pierre-Marie de Rodat Dec. 2, 2021, 4:28 p.m. UTC 
Description of Activation_Is_Complete was amended in AI12-0231-1. This
routine raises a Program_Error when called with Null_Task_Id. Add an
explicit contract to make GNATprove aware of the restriction.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnarl/a-taside.ads (Activation_Is_Complete): Add
	precondition.
diff mbox series

Patch

diff --git a/gcc/ada/libgnarl/a-taside.ads b/gcc/ada/libgnarl/a-taside.ads
--- 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