blob: c3a42e6b83c36bae92acb8f53b7207f999554b22 (
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
|
//Translation from feedback_diverge.c
//Should give an error
//Not sure on this one...
procedure main() returns () {
var A : float;
var B : float;
var X : float;
var i : int;
var rand : int;
A := fp(0);
B := fp(0);
i := 0;
while (i < 3600000) {
havoc rand;
if (rand != 0) {
havoc X;
assume(X >= fp(-20) && X <= fp(20));
}
else {
X := B;
}
B := B - (B * fp(2.0) - A - X) * fp(.005);
A := X;
i := i + 1;
}
assert(A >= fp(-100) && A <= fp(100));
}
|