blob: de14842491d92938ad22bc738460df4a8cba3bb5 (
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 (float24e8);
function {:builtin "(_ to_fp 8 24) RNE"} TO_FLOAT32_REAL(real) returns (float24e8);
procedure main() returns () {
var tick : float24e8;
var time : float24e8;
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);
}
|
