1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
CoResolution.dfy(18,11): Error: member Undeclared# does not exist in class TestClass
CoResolution.dfy(19,6): Error: unresolved identifier: Undeclared#
CoResolution.dfy(22,9): Error: unresolved identifier: _k
CoResolution.dfy(41,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)
CoResolution.dfy(52,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(70,12): Error: a copredicate is not allowed to declare any reads clause
CoResolution.dfy(76,33): Error: a copredicate is not allowed to declare any ensures clause
CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(90,20): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(99,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(113,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(114,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(119,24): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(125,28): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(133,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(134,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(139,26): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(145,30): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(153,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(155,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(171,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
CoResolution.dfy(206,12): Error: type variable '_T0' in the function call to 'A' could not be determined
CoResolution.dfy(206,13): Error: the type of this expression is underspecified
CoResolution.dfy(206,19): Error: type variable '_T0' in the function call to 'S' could not be determined
24 resolution/type errors detected in CoResolution.dfy
|
