mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
e6a11b4b11
support for unary -, div and mod in logic support for <-> in logic support for calls inside conditions of if and while support for `check` fixed compilation warnings
22 lines
311 B
Plaintext
22 lines
311 B
Plaintext
|
|
use int.Int
|
|
use bool.Bool
|
|
|
|
val ref exit : bool
|
|
val ref c : int
|
|
|
|
let test [@bddinfer] () diverges =
|
|
exit <- false;
|
|
c <- 0;
|
|
[@bddinfer:myloop]
|
|
while (not exit) do
|
|
[@bddinfer:myassert] assert { c <= 42 };
|
|
c <- c + 1;
|
|
if c >= 42 then
|
|
begin
|
|
exit <- true;
|
|
(* break*)
|
|
end
|
|
|
|
done
|