gnatprove_13.2.1_28fc3583/share/examples/spark/adacore_u/Concurrency/trivial.adb

 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;