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/CoResolution.dfy.expect | |
| parent | dc0a9130355352d0f47e07232d8119fc7219ccbc (diff) | |
Set up the same test infrastructure as in Boogie.
Diffstat (limited to 'Test/dafny0/CoResolution.dfy.expect')
| -rw-r--r-- | Test/dafny0/CoResolution.dfy.expect | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect new file mode 100644 index 00000000..423bf928 --- /dev/null +++ b/Test/dafny0/CoResolution.dfy.expect @@ -0,0 +1,22 @@ +CoResolution.dfy(17,9): Error: member Undeclared# does not exist in class _default
+CoResolution.dfy(18,4): Error: unresolved identifier: Undeclared#
+CoResolution.dfy(21,7): Error: unresolved identifier: _k
+CoResolution.dfy(39,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
+CoResolution.dfy(50,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+CoResolution.dfy(67,10): Error: a copredicate is not allowed to declare any reads clause
+CoResolution.dfy(73,31): Error: a copredicate is not allowed to declare any ensures clause
+CoResolution.dfy(82,20): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(95,4): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(109,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(110,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(115,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(121,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(129,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(130,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+CoResolution.dfy(135,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+21 resolution/type errors detected in c:\codeplex\dafny\Test\dafny0\CoResolution.dfy
|