1-- { dg-do compile } 2 3procedure SPARK3 (X : in out Integer) with SPARK_Mode is 4 5 procedure Q (X : in out Integer) with SPARK_Mode => Off is 6 begin 7 X := X + 1; 8 end Q; 9 10 procedure R (X : in out Integer); 11 12 procedure R (X : in out Integer) with SPARK_Mode => Off is 13 begin 14 Q (X); 15 end R; 16 17begin 18 R (X); 19 X := X + 1; 20end SPARK3; 21