[Ada] Add contract to Ada.Task_Identification.Activation_Is_Complete
Commit Message
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.
@@ -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