21 lines
351 B
Ada
21 lines
351 B
Ada
-- { dg-do compile }
|
|
-- { dg-options "-gnatd.F -gnatwa" }
|
|
|
|
with Ada.Dispatching;
|
|
|
|
procedure Contract1 with SPARK_Mode is
|
|
|
|
function Foo return Boolean is
|
|
begin
|
|
Ada.Dispatching.Yield;
|
|
return True;
|
|
end Foo;
|
|
|
|
Dummy : constant Integer := 0;
|
|
|
|
begin
|
|
if Foo and then True then
|
|
raise Program_Error;
|
|
end if;
|
|
end Contract1;
|