diff options
| author |  Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
| commit | e67c951ad9c5c637e36a6f025ba3d6e3ad945416 (patch) | |
| tree | 0cfb5c339602e4bdebf4bf97f3f0ccc3923c14d1 /Test/dafny0/UnfoldingPerformance.dfy | |
| parent | 000aa762e1fee4b9bd83ec3d7c8b61fd203e2c9d (diff) | |
| parent | df5c5f547990c1f80ab7594a1f9287ee03a61754 (diff) | |
Merge commit 'df5c5f5'
Diffstat (limited to 'Test/dafny0/UnfoldingPerformance.dfy')
| -rw-r--r-- | Test/dafny0/UnfoldingPerformance.dfy | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/Test/dafny0/UnfoldingPerformance.dfy b/Test/dafny0/UnfoldingPerformance.dfy new file mode 100644 index 00000000..3eed689a --- /dev/null +++ b/Test/dafny0/UnfoldingPerformance.dfy @@ -0,0 +1,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?
+}
|