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
|
TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
TypeTests.dfy(178,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost
TypeTests.dfy(188,6): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(189,9): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(207,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(213,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
TypeTests.dfy(220,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, got int)
TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
TypeTests.dfy(61,8): Error: Duplicate local-variable name: x
TypeTests.dfy(64,6): Error: Duplicate local-variable name: y
TypeTests.dfy(70,11): Error: unresolved identifier: x
TypeTests.dfy(72,28): Error: unresolved identifier: z
TypeTests.dfy(73,29): Error: unresolved identifier: w1
TypeTests.dfy(73,47): Error: unresolved identifier: w0
TypeTests.dfy(76,28): Error: unresolved identifier: e
TypeTests.dfy(91,17): Error: object initialization must denote an initializing method or constructor (F)
TypeTests.dfy(92,17): Error: a method called as an initialization method must not have any result arguments
TypeTests.dfy(101,3): Error: cannot assign to a range of array elements (try the 'forall' statement)
TypeTests.dfy(102,3): Error: cannot assign to a range of array elements (try the 'forall' statement)
TypeTests.dfy(103,3): Error: cannot assign to a range of array elements (try the 'forall' statement)
TypeTests.dfy(105,3): Error: cannot assign to a range of array elements (try the 'forall' statement)
TypeTests.dfy(106,3): Error: cannot assign to a range of array elements (try the 'forall' statement)
TypeTests.dfy(107,3): Error: cannot assign to a range of array elements (try the 'forall' statement)
TypeTests.dfy(113,6): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(114,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(115,8): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(116,8): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(119,28): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(119,28): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(120,17): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(120,10): Error: new can be applied only to reference types (got Expl_Class<nat>)
TypeTests.dfy(121,17): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(124,6): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(125,6): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(126,6): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(127,6): Error: sorry, cannot instantiate collection type with a subrange type
TypeTests.dfy(128,13): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(129,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(130,10): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(134,11): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(135,11): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(138,14): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(139,14): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(140,20): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(143,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(144,22): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(147,12): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(148,12): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(150,5): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
62 resolution/type errors detected in TypeTests.dfy
|
