forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ParameterResolution.dfy.expect
103 lines (103 loc) · 12.7 KB
/
ParameterResolution.dfy.expect
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
ParameterResolution.dfy(17,15): Error: wrong number of arguments (got 2, but function 'F' expects 3: (x: int, y: int, z: int))
ParameterResolution.dfy(18,15): Error: wrong number of arguments (got 4, but function 'F' expects 3: (x: int, y: int, z: int))
ParameterResolution.dfy(19,27): Error: duplicate binding for parameter name 'y'
ParameterResolution.dfy(19,15): Error: function parameter 'z' at index 2 requires an argument of type int
ParameterResolution.dfy(20,19): Error: the parameter named 'x' is already given positionally
ParameterResolution.dfy(20,15): Error: function parameter 'z' at index 2 requires an argument of type int
ParameterResolution.dfy(21,27): Error: a positional argument is not allowed to follow named arguments
ParameterResolution.dfy(21,15): Error: function parameter 'z' at index 2 requires an argument of type int
ParameterResolution.dfy(27,22): Error: the binding named 'xyz' does not correspond to any formal parameter
ParameterResolution.dfy(27,15): Error: function parameter 'z' at index 2 requires an argument of type int
ParameterResolution.dfy(30,14): Error: datatype constructor parameter at index 1 requires an argument of type bool
ParameterResolution.dfy(31,34): Error: the parameter named 'a' is already given positionally
ParameterResolution.dfy(31,14): Error: datatype constructor parameter at index 1 requires an argument of type bool
ParameterResolution.dfy(41,24): Error: default-value expression (of type 'bool') is not assignable to formal (of type 'int')
ParameterResolution.dfy(51,34): Error: 'this' is not allowed in a 'static' context
ParameterResolution.dfy(52,42): Error: 'this' is not allowed in a 'static' context
ParameterResolution.dfy(53,31): Error: 'this' is not allowed in a 'static' context
ParameterResolution.dfy(53,35): Error: 'this' is not allowed in a 'static' context
ParameterResolution.dfy(53,44): Error: 'this' is not allowed in a 'static' context
ParameterResolution.dfy(53,48): Error: 'this' is not allowed in a 'static' context
ParameterResolution.dfy(54,29): Error: 'this' is not allowed in a 'static' context
ParameterResolution.dfy(58,39): Error: unresolved identifier: b
ParameterResolution.dfy(60,12): Error: default-value expressions for parameters contain a cycle: x -> x
ParameterResolution.dfy(62,12): Error: default-value expressions for parameters contain a cycle: x -> y -> z -> x
ParameterResolution.dfy(66,24): Error: default-valued expressions are cyclicly dependent; this is not allowed, since it would cause infinite expansion
ParameterResolution.dfy(68,30): Error: default-valued expressions are cyclicly dependent; this is not allowed, since it would cause infinite expansion
ParameterResolution.dfy(68,30): Error: default-valued expressions are cyclicly dependent; this is not allowed, since it would cause infinite expansion
ParameterResolution.dfy(68,45): Error: default-valued expressions are cyclicly dependent; this is not allowed, since it would cause infinite expansion
ParameterResolution.dfy(73,62): Error: default-valued expressions are cyclicly dependent; this is not allowed, since it would cause infinite expansion
ParameterResolution.dfy(74,54): Error: default-valued expressions are cyclicly dependent; this is not allowed, since it would cause infinite expansion
ParameterResolution.dfy(99,89): Error: ghost variables such as x are allowed only in specification contexts. x was inferred to be ghost based on its declaration or initialization.
ParameterResolution.dfy(101,89): Error: ghost variables such as x are allowed only in specification contexts. x was inferred to be ghost based on its declaration or initialization.
ParameterResolution.dfy(104,27): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization.
ParameterResolution.dfy(109,32): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization.
ParameterResolution.dfy(79,22): Error: ghost variables such as y are allowed only in specification contexts. y was inferred to be ghost based on its declaration or initialization.
ParameterResolution.dfy(86,52): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
ParameterResolution.dfy(88,58): Error: a call to a ghost function is allowed only in specification contexts (consider declaring the function without the 'ghost' keyword)
ParameterResolution.dfy(95,89): Error: ghost variables such as x are allowed only in specification contexts. x was inferred to be ghost based on its declaration or initialization.
ParameterResolution.dfy(97,82): Error: ghost variables such as x are allowed only in specification contexts. x was inferred to be ghost based on its declaration or initialization.
ParameterResolution.dfy(127,14): Error: wrong number of arguments (got 0, but function 'N' expects 1: (x: int))
ParameterResolution.dfy(133,14): Error: wrong number of arguments (got 0, but function 'O' expects 1: (x: int))
ParameterResolution.dfy(147,12): Error: wrong number of arguments (got 0, but function 'O' expects 1: (x: int))
ParameterResolution.dfy(161,13): Error: a refining formal parameter ('x') in a refinement module is not allowed to give a default-value expression
ParameterResolution.dfy(163,13): Error: a refining formal parameter ('x') in a refinement module is not allowed to give a default-value expression
ParameterResolution.dfy(172,14): Error: a refining formal parameter ('x') in a refinement module is not allowed to give a default-value expression
ParameterResolution.dfy(174,12): Error: a refining formal parameter ('x') in a refinement module is not allowed to give a default-value expression
ParameterResolution.dfy(169,12): Error: wrong number of arguments (got 0, but function 'O' expects 1: (x: int))
ParameterResolution.dfy[RefinementB](147,12): Error: wrong number of arguments (got 0, but function 'O' expects 1: (x: int))
ParameterResolution.dfy(197,26): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
ParameterResolution.dfy(197,26): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
ParameterResolution.dfy(198,37): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
ParameterResolution.dfy(193,21): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
ParameterResolution.dfy(194,13): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
ParameterResolution.dfy(196,29): Error: type parameter 'X' (inferred to be '?') in the function call to 'F' could not be determined
ParameterResolution.dfy(211,23): Error: old expressions are not allowed in this context
ParameterResolution.dfy(213,25): Error: old expressions are not allowed in this context
ParameterResolution.dfy(216,32): Error: old expressions are not allowed in this context
ParameterResolution.dfy(217,33): Error: old expressions are not allowed in this context
ParameterResolution.dfy(225,14): Error: the name 'Nothing' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Ax.Nothing')
ParameterResolution.dfy(226,14): Error: the name 'Nothing' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Ax.Nothing')
ParameterResolution.dfy(227,14): Error: the name 'Nothing' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Ax.Nothing')
ParameterResolution.dfy(239,17): Error: wrong number of arguments (got 2, but datatype constructor 'Create' expects at most 1: (x: int))
ParameterResolution.dfy(246,5): Error: method in-parameter 'a' at index 0 requires an argument of type int
ParameterResolution.dfy(246,5): Error: method in-parameter 'b' at index 1 requires an argument of type int
ParameterResolution.dfy(247,5): Error: method in-parameter 'a' at index 0 requires an argument of type int
ParameterResolution.dfy(247,5): Error: method in-parameter 'b' at index 1 requires an argument of type int
ParameterResolution.dfy(252,21): Error: Duplicate parameter name: x
ParameterResolution.dfy(259,11): Error: default-value expressions for parameters contain a cycle: x -> x
ParameterResolution.dfy(260,35): Error: unresolved identifier: _k
ParameterResolution.dfy(261,26): Error: unresolved identifier: _k
ParameterResolution.dfy(278,33): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'u'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(278,33): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'u'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(281,45): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter '1'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(284,27): Error: because of a later nameless parameter, this default value is never used; remove it or name all subsequent parameters
ParameterResolution.dfy(285,39): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'b'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(286,34): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'b'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(368,79): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'baz'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(290,21): Error: nameonly parameter 'c' must be passed using a name binding; it cannot be passed positionally
ParameterResolution.dfy(297,26): Error: nameonly parameter 'c' must be passed using a name binding; it cannot be passed positionally
ParameterResolution.dfy(301,34): Error: a positional argument is not allowed to follow named arguments
ParameterResolution.dfy(305,23): Error: nameonly parameter 'b' must be passed using a name binding; it cannot be passed positionally
ParameterResolution.dfy(308,28): Error: the binding named 'unknown' does not correspond to any formal parameter
ParameterResolution.dfy(312,19): Error: a positional argument is not allowed to follow named arguments
ParameterResolution.dfy(313,11): Error: nameonly parameter 'b' must be passed using a name binding; it cannot be passed positionally
ParameterResolution.dfy(313,16): Error: the parameter named 'b' is already given positionally
ParameterResolution.dfy(314,21): Error: duplicate binding for parameter name 'b'
ParameterResolution.dfy(323,16): Error: nameonly parameter 'b' must be passed using a name binding; it cannot be passed positionally
ParameterResolution.dfy(328,15): Error: wrong number of arguments (got 1, but least predicate 'LP' expects at least 2: (a: int, b: int, c: int))
ParameterResolution.dfy(329,15): Error: least predicate parameter 'b' at index 1 requires an argument of type int
ParameterResolution.dfy(333,36): Error: the parameter named 'a' is already given positionally
ParameterResolution.dfy(336,21): Error: nameonly parameter 'u' must be passed using a name binding; it cannot be passed positionally
ParameterResolution.dfy(337,29): Error: a positional argument is not allowed to follow named arguments
ParameterResolution.dfy(337,12): Error: constructor in-parameter 'x' at index 1 requires an argument of type int
ParameterResolution.dfy(340,37): Error: duplicate binding for parameter name 'x'
ParameterResolution.dfy(343,12): Error: unresolved identifier: a
ParameterResolution.dfy(351,15): Error: nameonly parameter '900' must be passed using a name binding; it cannot be passed positionally
ParameterResolution.dfy(355,15): Error: the binding named '0900' does not correspond to any formal parameter
ParameterResolution.dfy(355,9): Error: datatype constructor parameter '900' at index 1 requires an argument of type int
ParameterResolution.dfy(356,25): Error: the binding named '90_0' does not correspond to any formal parameter
ParameterResolution.dfy(369,73): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'baz'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(370,71): Error: this parameter is effectively nameonly (because of the earlier nameonly parameter 'baz'); declare it as nameonly or give it an default-value expression
ParameterResolution.dfy(377,9): Error: wrong number of arguments (got 0, but datatype constructor 'Foo' expects at least 1: (bar: string, baz: string, qux: int))
102 resolution/type errors detected in ParameterResolution.dfy