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 --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