mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
15 lines
241 B
Plaintext
15 lines
241 B
Plaintext
module SimpleLoop
|
|
use int.Int
|
|
let cfg simple_loop () : int =
|
|
var x : int;
|
|
{ x <- 0; goto L0 }
|
|
L0 { x<- 3; switch (x < 10)
|
|
| True -> goto R
|
|
| False -> goto L1
|
|
end
|
|
}
|
|
L1 { x <- 10; goto L0 }
|
|
S { return x }
|
|
R { x <- x + 1; goto S }
|
|
end
|