aboutsummaryrefslogtreecommitdiff
path: root/gcc/testsuite/gnat.dg/protected_func.adb
blob: 055bf5dd12d162dedeed6ea0c2b7e8604fb1b3fd (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
--  { dg-do compile }

package body Protected_Func with SPARK_Mode is
   protected body Prot_Obj is
      function Prot_Func return Integer is
      begin
         Comp := Comp + 1;  --  { dg-error "protected function cannot modify its protected object" }
         Part_Of_Constit := Part_Of_Constit + 1;  --  { dg-error "protected function cannot modify its protected object" }

         return Comp + Part_Of_Constit;
      end Prot_Func;
   end Prot_Obj;
end Protected_Func;