blob: 3eed689a60a543156091a186a41089d5680cab7e (
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
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
// RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class C {
var x: nat
function method IgnoreFuel(): nat
reads this
{
x
}
}
function method Fib(n: int): int
{
if n < 2 then n else Fib(n-2) + Fib(n-1)
}
method Test0() {
var c := new C;
var f := Fib(c.IgnoreFuel());
// with the bug, the following wwould take a long time before it reports an error
// after the bug fix, this still fails, but quickly
assert 0 <= f;
}
method Test1() {
var c := new C;
var f := Fib(c.x);
// the following assert will also fail, but quickly
assert 0 <= f;
}
method Test2() {
var c := new C;
c.x := 10;
var f := Fib(c.IgnoreFuel());
assert 0 <= f; // passes
}
method Test3() {
var c := new C;
c.x := 10;
var f := Fib(c.x);
assert 0 <= f; // passes
}
method Test4() {
var c := new C;
c.x := 10;
var f := Fib(c.x - 2);
assert 0 <= f; // fails
}
method Test5(x: int)
requires 9 <= x - 1 && x + 1 <= 11
{
var c := new C;
c.x := x;
var f := Fib(c.x);
assert 0 <= f; // succeeds?
}
|
