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


Reply via email to