gcc/testsuite/gnat.dg/protected_func.ads

   1 package Protected_Func with SPARK_Mode is
   2    protected Prot_Obj is
   3       function Prot_Func return Integer;
   4    private
   5       Comp : Integer := 0;
   6    end Prot_Obj;
   7
   8    Part_Of_Constit : Integer := 0 with Part_Of => Prot_Obj;
   9 end Protected_Func;