diff options
| author |  wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
|---|---|---|
| committer | wuestholz <unknown> | 2014-05-29 21:41:00 +0200 |
| commit | 607ef28aadb281ab61a2be493a637126e967a388 (patch) | |
| tree | aae16c049c860e443920f9c6ee31af4e35f8a800 /Test/dafny0/IteratorResolution.dfy.expect | |
| parent | dc0a9130355352d0f47e07232d8119fc7219ccbc (diff) | |
Set up the same test infrastructure as in Boogie.
Diffstat (limited to 'Test/dafny0/IteratorResolution.dfy.expect')
| -rw-r--r-- | Test/dafny0/IteratorResolution.dfy.expect | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/IteratorResolution.dfy.expect b/Test/dafny0/IteratorResolution.dfy.expect new file mode 100644 index 00000000..25890cd9 --- /dev/null +++ b/Test/dafny0/IteratorResolution.dfy.expect @@ -0,0 +1,13 @@ +IteratorResolution.dfy(62,9): Error: LHS of assignment must denote a mutable field
+IteratorResolution.dfy(67,18): Error: arguments must have the same type (got _T0 and int)
+IteratorResolution.dfy(79,19): Error: RHS (of type bool) not assignable to LHS (of type int)
+IteratorResolution.dfy(82,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called
+IteratorResolution.dfy(86,15): Error: logical negation expects a boolean argument (instead got int)
+IteratorResolution.dfy(20,9): Error: LHS of assignment must denote a mutable field
+IteratorResolution.dfy(22,9): Error: LHS of assignment must denote a mutable field
+IteratorResolution.dfy(126,9): Error: unresolved identifier: _decreases3
+IteratorResolution.dfy(127,21): Error: arguments must have the same type (got int and ?)
+IteratorResolution.dfy(128,2): Error: LHS of assignment must denote a mutable field
+IteratorResolution.dfy(135,9): Error: unresolved identifier: _decreases1
+IteratorResolution.dfy(140,9): Error: unresolved identifier: _decreases0
+12 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\IteratorResolution.dfy
|