gcc/testsuite/gnat.dg/protected_func.adb

   1 --  { dg-do compile }
   2
   3 package body Protected_Func with SPARK_Mode is
   4    protected body Prot_Obj is
   5       function Prot_Func return Integer is
   6       begin
   7          Comp := Comp + 1;  --  { dg-error "protected function cannot modify its protected object" }
   8          Part_Of_Constit := Part_Of_Constit + 1;  --  { dg-error "protected function cannot modify its protected object" }
   9
  10          return Comp + Part_Of_Constit;
  11       end Prot_Func;
  12    end Prot_Obj;
  13 end Protected_Func;