mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
26 lines
365 B
Plaintext
26 lines
365 B
Plaintext
module Anders_Find
|
|
use int.Int
|
|
let rec cfg find [@cfg:stackify] [@cfg:subregion_analysis] (key : int) : int
|
|
|
|
=
|
|
var cnt : int;
|
|
{
|
|
cnt <- key;
|
|
goto BB0
|
|
}
|
|
BB0 {
|
|
variant { cnt };
|
|
switch (cnt > 0)
|
|
| True -> goto BB1
|
|
| False -> goto Exit
|
|
end
|
|
}
|
|
BB1 {
|
|
cnt <- cnt - 1;
|
|
goto BB0
|
|
}
|
|
Exit {
|
|
return 0
|
|
}
|
|
|
|
end |