blob: a31aa21557324e069c32f201c75b316086ea3468 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
//Translation from drift_tenth.c
//Should Fail
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;
//}
time := time + tick;//1
time := time + tick;//2
time := time + tick;//3
time := time + tick;//4
time := time + tick;//5
time := time + tick;//6
time := time + tick;//7
time := time + tick;//8
time := time + tick;//9
time := time + tick;//10
assert time == TO_FLOAT32_INT(1);
}
|
