blob: 7536f8fd012d7fa6f42087ac247b1a2169b0d0bb (
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
33
34
35
36
|
//Translation from filter1.c
//Should Verify
function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_INT(int) returns (float64);
function {:builtin "(_ to_fp 11 53) RNE"} TO_FLOAT64_REAL(real) returns (float64);
procedure main() returns () {
var E0 : float64;
var E1 : float64;
var S : float64);
var i : int;
var rand : int;
E1 := TO_FLOAT64_INT(0);
S := TO_FLOAT64_INT(0);
i := 0;
while (i <= 1000000)
{
havoc E0;
assume(E0 >= fp(-1 11 53) && E0 <= fp(1 11 53));
havoc rand;
if (rand != 0) {
S := fp(0 11 53);
}
else {
S := fp(0.999 11 53) * S + E0 - E1;
}
E1 := E0;
//assert(1==0);
assert(S >= fp(-1 11 53) && S <= fp(1 11 53));
i := i + 1;
}
}
|
