diff options
| author |  wuestholz <unknown> | 2012-01-24 16:41:59 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2012-01-24 16:41:59 +0100 |
| commit | 1058d7e8c966b521bcda4f02f448d63d823b1bf3 (patch) | |
| tree | 285e2b87d700460c1e980ac3cdbd5267d986820a | |
| parent | a8abac3364f9af380d9854b490426c1a3b016d97 (diff) | |
Dafny: Fixed a bug in the printing of let expressions.
| -rw-r--r-- | Dafny/Printer.cs | 1 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 20 | ||||
| -rw-r--r-- | Test/dafny0/LetExpr.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 2 |
4 files changed, 23 insertions, 2 deletions
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index f98f7cbe..9bd29da0 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -1080,6 +1080,7 @@ namespace Microsoft.Dafny { var e = (LetExpr)expr;
bool parensNeeded = !isRightmost;
if (parensNeeded) { wr.Write("("); }
+ wr.Write("var ");
string sep = "";
foreach (var v in e.Vars) {
wr.Write("{0}{1}", sep, v.Name);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7baa5817..6f160a66 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1674,3 +1674,23 @@ Execution trace: (0,0): anon6_Else
Dafny program verifier finished with 58 verified, 21 errors
+
+-------------------- LetExpr.dfy --------------------
+LetExpr.dfy(5,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+LetExpr.dfy(104,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+
+Dafny program verifier finished with 13 verified, 2 errors
+out.tmp.dfy(10,12): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+out.tmp.dfy(101,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+
+Dafny program verifier finished with 13 verified, 2 errors
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 703813d2..48e4810b 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -1,5 +1,5 @@ method M0(n: int)
- requires var f := 100; n < f;
+ requires var f := 100; n < f; requires var t, f := true, false; (t && f) || n < 100;
{
assert n < 200;
assert 0 <= n; // error
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index 0da3b411..d09e1cc2 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -27,7 +27,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy %DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
)
-for %%f in (SmallTests.dfy) do (
+for %%f in (SmallTests.dfy LetExpr.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /dprint:out.tmp.dfy %* %%f
|