File: simple_loop.mlcfg

package info (click to toggle)
why3 1.8.2-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 45,020 kB
  • sloc: xml: 185,443; ml: 111,224; ansic: 3,998; sh: 2,578; makefile: 2,568; java: 865; python: 720; javascript: 290; lisp: 205; pascal: 173
file content (14 lines) | stat: -rw-r--r-- 241 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
 
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