Skip to content

Commit 4e591de

Browse files
LinyxusLinyxus
committed
Update checkfiles for CC tests
1 parent 19ffcb3 commit 4e591de

13 files changed

+233
-93
lines changed

‎tests/neg-custom-args/captures/consume-in-constructor.check‎

Lines changed: 23 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,32 @@
11
-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 --------------------------------------------
2+
Separation failure: Illegal access to (b : B^), which was passed as a consume parameter to constructor of class A2
3+
and therefore is no longer available.
4+
5+
where: ^ refers to a fresh root capability in the type of value b
6+
18 | val a2 = A2(b)
7+
| -
8+
| The capability was consumed here.
9+
19 | val _: A2^{cap, b} = a2
210
20 | println(b) // error
311
| ^
4-
|Separation failure: Illegal access to (b : B^), which was passed as a consume parameter to constructor of class A2
5-
|on line 18 and therefore is no longer available.
6-
|
7-
|where: ^ refers to a fresh root capability in the type of value b
12+
| Then, it was used here
13+
814
-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:21:10 --------------------------------------------
15+
Separation failure: Illegal access to (a1 : A1{val b: B^{b²}}^{cap, b²}), which was passed as a consume parameter to constructor of class A2
16+
and therefore is no longer available.
17+
18+
where: b is a value in class A1
19+
b² is a value in method Test
20+
cap is a fresh root capability in the type of value a1
21+
18 | val a2 = A2(b)
22+
| -
23+
| The capability was consumed here.
24+
19 | val _: A2^{cap, b} = a2
25+
20 | println(b) // error
926
21 | println(a1) // error, since `b` was consumed before
1027
| ^^
11-
|Separation failure: Illegal access to (a1 : A1{val b: B^{b²}}^{cap, b²}), which was passed as a consume parameter to constructor of class A2
12-
|on line 18 and therefore is no longer available.
13-
|
14-
|where: b is a value in class A1
15-
| b² is a value in method Test
16-
| cap is a fresh root capability in the type of value a1
28+
| Then, it was used here
29+
1730
-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:27:10 --------------------------------------------
1831
27 | println(b) // error, b is hidden in the type of a1
1932
| ^

‎tests/neg-custom-args/captures/consume-twice-same-line.check‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 ---------------------------------------
1+
-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 --------------------------------------------
22
Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
33
and therefore is no longer available.
44

@@ -8,7 +8,7 @@ where: ^ refers to a fresh root capability in the type of parameter x
88
| | Then, it was used here
99
| The capability was consumed here.
1010

11-
-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 ---------------------------------------
11+
-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 --------------------------------------------
1212
Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
1313
and therefore is no longer available.
1414

@@ -18,7 +18,7 @@ where: ^ refers to a fresh root capability in the type of parameter x
1818
| | Then, it was used here
1919
| The capability was consumed here.
2020

21-
-- Type Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 ---------------------------------------
21+
-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 --------------------------------------------
2222
Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
2323
and therefore is no longer available.
2424

‎tests/neg-custom-args/captures/consume-twice.check‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
-- Type Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 --------------------------------------------------
1+
-- Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 -------------------------------------------------------
22
Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
33
and therefore is no longer available.
44

‎tests/neg-custom-args/captures/i24373.check‎

Lines changed: 27 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,36 @@
11
-- Error: tests/neg-custom-args/captures/i24373.scala:28:2 -------------------------------------------------------------
2+
Separation failure: Illegal access to (x1 : Foo^), which was used as a prefix to consume method sink1
3+
and therefore is no longer available.
4+
5+
where: ^ refers to a fresh root capability in the type of value x1
6+
27 | x1.sink1
7+
| --
8+
| The capability was consumed here.
29
28 | x1.sink1 // error
310
| ^^
4-
| Separation failure: Illegal access to (x1 : Foo^), which was used as a prefix to consume method sink1
5-
| on line 27 and therefore is no longer available.
6-
|
7-
| where: ^ refers to a fresh root capability in the type of value x1
11+
| Then, it was used here
12+
813
-- Error: tests/neg-custom-args/captures/i24373.scala:32:2 -------------------------------------------------------------
14+
Separation failure: Illegal access to (x2 : Bar^), which was used as a prefix to consume method sink2
15+
and therefore is no longer available.
16+
17+
where: ^ refers to a fresh root capability in the type of value x2
18+
31 | x2.sink2
19+
| --
20+
| The capability was consumed here.
921
32 | x2.sink2 // error
1022
| ^^
11-
| Separation failure: Illegal access to (x2 : Bar^), which was used as a prefix to consume method sink2
12-
| on line 31 and therefore is no longer available.
13-
|
14-
| where: ^ refers to a fresh root capability in the type of value x2
23+
| Then, it was used here
24+
1525
-- Error: tests/neg-custom-args/captures/i24373.scala:49:8 -------------------------------------------------------------
26+
Separation failure: Illegal access to (x6 : Bar^), which was passed as a consume parameter to method sink6
27+
and therefore is no longer available.
28+
29+
where: ^ refers to a fresh root capability in the type of value x6
30+
48 | sink6(x6)
31+
| --
32+
| The capability was consumed here.
1633
49 | sink6(x6) // error
1734
| ^^
18-
| Separation failure: Illegal access to (x6 : Bar^), which was passed as a consume parameter to method sink6
19-
| on line 48 and therefore is no longer available.
20-
|
21-
| where: ^ refers to a fresh root capability in the type of value x6
35+
| Then, it was used here
36+

‎tests/neg-custom-args/captures/i24373a.check‎

Lines changed: 54 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,38 +1,72 @@
11
-- Error: tests/neg-custom-args/captures/i24373a.scala:15:8 ------------------------------------------------------------
2+
Separation failure: Illegal access to (x1 : Bar^), which was passed as a consume parameter to method sink1
3+
and therefore is no longer available.
4+
5+
where: ^ refers to a fresh root capability in the type of value x1
6+
13 | sink1(x1)
7+
| --
8+
| The capability was consumed here.
9+
14 | sink1(x1) // ok, rd/rd
210
15 | sink2(x1) // error
311
| ^^
4-
| Separation failure: Illegal access to (x1 : Bar^), which was passed as a consume parameter to method sink1
5-
| on line 13 and therefore is no longer available.
6-
|
7-
| where: ^ refers to a fresh root capability in the type of value x1
12+
| Then, it was used here
13+
814
-- Error: tests/neg-custom-args/captures/i24373a.scala:19:8 ------------------------------------------------------------
15+
Separation failure: Illegal access to x2.rd, which was passed as a consume parameter to method sink2
16+
and therefore is no longer available.
17+
18 | sink2(x2)
18+
| --
19+
| The capability was consumed here.
920
19 | sink1(x2) // error
1021
| ^^
11-
| Separation failure: Illegal access to x2.rd, which was passed as a consume parameter to method sink2
12-
| on line 18 and therefore is no longer available.
22+
| Then, it was used here
23+
1324
-- Error: tests/neg-custom-args/captures/i24373a.scala:20:8 ------------------------------------------------------------
25+
Separation failure: Illegal access to (x2 : Bar^), which was passed as a consume parameter to method sink2
26+
and therefore is no longer available.
27+
28+
where: ^ refers to a fresh root capability in the type of value x2
29+
18 | sink2(x2)
30+
| --
31+
| The capability was consumed here.
32+
19 | sink1(x2) // error
1433
20 | sink2(x2) // error
1534
| ^^
16-
| Separation failure: Illegal access to (x2 : Bar^), which was passed as a consume parameter to method sink2
17-
| on line 18 and therefore is no longer available.
18-
|
19-
| where: ^ refers to a fresh root capability in the type of value x2
35+
| Then, it was used here
36+
2037
-- Error: tests/neg-custom-args/captures/i24373a.scala:25:8 ------------------------------------------------------------
38+
Separation failure: Illegal access to (x3 : Bar^), which was passed as a consume parameter to method sink3
39+
and therefore is no longer available.
40+
41+
where: ^ refers to a fresh root capability in the type of value x3
42+
23 | sink3(x3)
43+
| --
44+
| The capability was consumed here.
45+
24 | sink3(x3) // ok, rd/rd
2146
25 | sink2(x3) // error
2247
| ^^
23-
| Separation failure: Illegal access to (x3 : Bar^), which was passed as a consume parameter to method sink3
24-
| on line 23 and therefore is no longer available.
25-
|
26-
| where: ^ refers to a fresh root capability in the type of value x3
48+
| Then, it was used here
49+
2750
-- Error: tests/neg-custom-args/captures/i24373a.scala:29:8 ------------------------------------------------------------
51+
Separation failure: Illegal access to x4.rd, which was passed as a consume parameter to method sink2
52+
and therefore is no longer available.
53+
28 | sink2(x4)
54+
| --
55+
| The capability was consumed here.
2856
29 | sink3(x4) // error
2957
| ^^
30-
| Separation failure: Illegal access to x4.rd, which was passed as a consume parameter to method sink2
31-
| on line 28 and therefore is no longer available.
58+
| Then, it was used here
59+
3260
-- Error: tests/neg-custom-args/captures/i24373a.scala:30:8 ------------------------------------------------------------
61+
Separation failure: Illegal access to (x4 : Bar^), which was passed as a consume parameter to method sink2
62+
and therefore is no longer available.
63+
64+
where: ^ refers to a fresh root capability in the type of value x4
65+
28 | sink2(x4)
66+
| --
67+
| The capability was consumed here.
68+
29 | sink3(x4) // error
3369
30 | sink2(x4) // error
3470
| ^^
35-
| Separation failure: Illegal access to (x4 : Bar^), which was passed as a consume parameter to method sink2
36-
| on line 28 and therefore is no longer available.
37-
|
38-
| where: ^ refers to a fresh root capability in the type of value x4
71+
| Then, it was used here
72+

‎tests/neg-custom-args/captures/lazyListState.check‎

Lines changed: 15 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,20 @@
11
-- [E164] Declaration Error: tests/neg-custom-args/captures/lazyListState.scala:12:39 ----------------------------------
2+
error overriding method tail in trait State of type -> LazyListIterable[A]^{cap};
3+
value tail of type LazyListIterable[A]^ has incompatible type
4+
5+
where: ^ refers to a fresh root capability in the type of value tail
6+
cap is a root capability associated with the result type of -> LazyListIterable[A²]^²
7+
5 | def tail: LazyListIterable[A]^
8+
| -
9+
| the overridden method is here
10+
6 |
11+
7 |private object State:
12+
8 | object Empty extends State[Nothing]:
13+
9 | def head: Nothing = throw new NoSuchElementException("head of empty lazy list")
14+
10 | def tail: LazyListIterable[Nothing] = throw new UnsupportedOperationException("tail of empty lazy list")
15+
11 |
216
12 | final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A] // error
317
| ^
4-
| error overriding method tail in trait State of type -> LazyListIterable[A]^{cap};
5-
| value tail of type LazyListIterable[A]^ has incompatible type
6-
|
7-
| where: ^ refers to a fresh root capability in the type of value tail
8-
| cap is a root capability associated with the result type of -> LazyListIterable[A²]^²
18+
| the overriding value has incompatible type
919
|
1020
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/lazylist.check‎

Lines changed: 21 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,11 +44,28 @@
4444
|
4545
| longer explanation available when compiling with `-explain`
4646
-- [E164] Declaration Error: tests/neg-custom-args/captures/lazylist.scala:22:6 ----------------------------------------
47+
error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing];
48+
method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type
49+
50+
where: cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
51+
8 | def tail: LazyList[T]
52+
| -
53+
| the overridden method is here
54+
9 |
55+
10 | def map[U](f: T => U): LazyList[U]^{f, this} =
56+
11 | if isEmpty then LazyNil
57+
12 | else LazyCons(f(head), () => tail.map(f))
58+
13 |
59+
14 |class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]:
60+
15 | def isEmpty = false
61+
16 | def head = x
62+
17 | def tail = xs() // error
63+
18 |
64+
19 |object LazyNil extends LazyList[Nothing]:
65+
20 | def isEmpty = true
66+
21 | def head = ???
4767
22 | def tail: LazyList[Nothing]^ = ??? // error overriding
4868
| ^
49-
| error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing];
50-
| method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type
51-
|
52-
| where: cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
69+
| the overriding method has incompatible type
5370
|
5471
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/mut-iterator1.check‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,13 @@
11
-- [E164] Declaration Error: tests/neg-custom-args/captures/mut-iterator1.scala:9:15 -----------------------------------
2+
error overriding method next in trait Iterator of type (): U;
3+
method next of type (): U is an update method, cannot override a read-only method
4+
5 | def next(): T
5+
| -
6+
| the overridden method is here
7+
6 |
8+
7 | def map[U](f: T => U): Iterator[U] = new Iterator:
9+
8 | def hasNext = Iterator.this.hasNext
210
9 | update def next() = f(Iterator.this.next()) // error
311
| ^
4-
| error overriding method next in trait Iterator of type (): U;
5-
| method next of type (): U is an update method, cannot override a read-only method
12+
| the overriding method is an update method, cannot override a read-only method
13+

‎tests/neg-custom-args/captures/sep-curried-par.check‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -34,12 +34,15 @@
3434
|where: => refers to a fresh root capability in the type of value p
3535
| =>² refers to a fresh root capability created in method test when checking argument to parameter p1 of method par
3636
-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:18:16 ---------------------------------------------------
37+
Separation failure: Illegal access to (p : () => Unit), which was passed as a consume parameter to method parCurried
38+
and therefore is no longer available.
39+
40+
where: => refers to a fresh root capability in the type of value p
3741
18 | parCurried(p)(p) // error: consume failure
38-
| ^
39-
|Separation failure: Illegal access to (p : () => Unit), which was passed as a consume parameter to method parCurried
40-
|on line 18 and therefore is no longer available.
41-
|
42-
|where: => refers to a fresh root capability in the type of value p
42+
| - ^
43+
| | Then, it was used here
44+
| The capability was consumed here.
45+
4346
-- Error: tests/neg-custom-args/captures/sep-curried-par.scala:21:9 ----------------------------------------------------
4447
21 | foo(c)(c) // error: separation
4548
| ^

‎tests/neg-custom-args/captures/sepchecks5.check‎

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,14 @@
99
| Separation failure: argument to consume parameter with type (io : Object^) refers to parameter io.
1010
| The parameter needs to be annotated with consume to allow this.
1111
-- Error: tests/neg-custom-args/captures/sepchecks5.scala:20:24 --------------------------------------------------------
12+
Separation failure: Illegal access to (io : Object^), which was passed as a consume parameter to method g
13+
and therefore is no longer available.
14+
15+
where: ^ refers to a fresh root capability in the type of parameter io
16+
19 | val f2 = g(io) // error
17+
| --
18+
| The capability was consumed here.
1219
20 | par(f2)(() => println(io)) // error
1320
| ^^
14-
| Separation failure: Illegal access to (io : Object^), which was passed as a consume parameter to method g
15-
| on line 19 and therefore is no longer available.
16-
|
17-
| where: ^ refers to a fresh root capability in the type of parameter io
21+
| Then, it was used here
22+

0 commit comments

Comments
 (0)