1 2 3 4 5 6 7 8 9 10 11 12 13 14 | with Ada.Task_Identification; use Ada.Task_Identification; package body Trivial with SPARK_Mode is Id : Task_Id; task body T is begin loop Id := Current_Task; end loop; end T; end Trivial; |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 | with Ada.Task_Identification; use Ada.Task_Identification; package body Trivial with SPARK_Mode is Id : Task_Id; task body T is begin loop Id := Current_Task; end loop; end T; end Trivial; |