diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 13:58:23 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 13:58:23 +0200 |
| commit | 3c789c793b917550c4d752307fc0e7496591fffe (patch) | |
| tree | 173af4bdd5eb13d24cf1a5cb58817a4f0cef99a6 /Test/dafny2 | |
| parent | 77a38428ffe11806c8bc61d2fbb324d1523de635 (diff) | |
Allow empty calc statements
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 8e3a4426..c48f2000 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -210,3 +210,9 @@ ghost method Window(xs: List, ys: List) true;
}
}
+
+// Empty calculations are also allowed, but they don't generate any Boogie code.
+ghost method Empty()
+{
+ calc {}
+}
|