repo.or.cz
/
why3.git
/
blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
log
|
graphiclog1
|
graphiclog2
|
commit
|
commitdiff
|
tree
|
refs
|
edit
|
fork
blame
|
history
|
raw
|
HEAD
fis sessions
[why3.git]
/
examples
/
mlcfg
/
break.mlcfg
blob
9d6af56aada591cd5f32d477fd9ed6bbbaeea55e
1
module NestedLoops
2
use int.Int
3
let cfg nested_loops x : () =
4
var a : int;
5
var b : int;
6
var c : int;
7
var d : int;
8
{
9
goto BB0
10
}
11
BB0 {
12
switch (true)
13
| True -> goto B
14
| False -> goto A
15
end
16
}
17
BB1 {
18
switch (True)
19
| True -> goto C
20
| False -> goto D
21
end
22
}
23
C {
24
c <- c + 1;
25
goto A
26
}
27
D {
28
d <- d + 1;
29
goto BB0
30
}
31
B {
32
b <- b + 1;
33
goto BB1
34
}
35
A {
36
a <- a + 1;
37
return ()
38
}
39
(*
40
loop i {
41
b
42
if j {
43
break;
44
}
45
d
46
}
47
a
48
*)
49
end