blob: ce5d2bc7f0757a93d693f670c84c45275571d382 (
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
|
//Translation from filter1.c
//Should Verify
procedure main() returns () {
var E0 : float(11 53);
var E1 : float(11 53);
var S : float(11 53);
var i : int;
var rand : int;
E1 := fp(0 11 53);
S := fp(0 11 53);
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;
}
}
|