blob: 424c5a2dcbaf6808b97da4c3f5aacb958885dbb5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
// RUN: %boogie -proverWarnings:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_INT(int) returns (float32);
function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float32);
procedure main() returns () {
var tick : float32;
var time : float32;
var i: int;
tick := TO_FLOAT32_INT(1)/TO_FLOAT32_INT(10);
time := TO_FLOAT32_INT(0);
i := 0;
while (i < 10)
{
time := time + tick;
i := i + 1;
}
assert time == TO_FLOAT32_INT(1);
}
|
