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;
|