diff options
| author |  Jason Koenig <unknown> | 2011-07-06 14:10:11 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-06 14:10:11 -0700 |
| commit | 89d9632457db76c9246b2d9cd88103238ad8f373 (patch) | |
| tree | b2bbd9f50e5195a9f4bcc799a7e24ebd8f62e843 /Test/dafny0/Answer | |
| parent | 80ec1a41fc8b7109c8fc45eff6d9acf29851562d (diff) | |
Dafny: Fixed bug in call statements where mutability of out parameters was not checked.
Added regression test.
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e5621773..a29c64fa 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1103,3 +1103,8 @@ Dafny program verifier finished with 16 verified, 0 errors -------------------- ChainingDisjointTests.dfy --------------------
Dafny program verifier finished with 6 verified, 0 errors
+
+-------------------- CallStmtTests.dfy --------------------
+CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable
+2 resolution/type errors detected in CallStmtTests.dfy
|