Skip to content

Commit 2ee70f2

Browse files
LinyxusLinyxus
committed
Update checkfiles
1 parent 7089e83 commit 2ee70f2

File tree

4 files changed

+120
-44
lines changed

4 files changed

+120
-44
lines changed

‎compiler/src/dotty/tools/dotc/reporting/messages.scala‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3742,8 +3742,9 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco
37423742
|
37433743
|In this case, the name `$name` is encoded as `${name.encode}`."""
37443744

3745-
class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context)
3746-
extends TypeMsg(NoExplanationID):
3745+
class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context) extends Message(NoExplanationID):
3746+
def kind = MessageKind.NoKind
3747+
37473748
protected def msg(using Context): String =
37483749
i"""Separation failure: Illegal access to $ref, which was $howConsumed
37493750
|and therefore is no longer available."""

‎tests/neg-custom-args/captures/linear-buffer-2.check‎

Lines changed: 44 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,59 @@
11
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 ---------------------------------------------------
2+
Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append
3+
and therefore is no longer available.
4+
5+
where: ^ refers to a fresh root capability in the type of parameter buf
6+
11 | val buf1: Buffer[Int]^ = buf.append(1)
7+
| ---
8+
| The capability was consumed here.
9+
12 | val buf2 = buf1.append(2) // OK
210
13 | val buf3 = buf.append(3) // error
311
| ^^^
4-
| Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append
5-
| on line 11 and therefore is no longer available.
6-
|
7-
| where: ^ refers to a fresh root capability in the type of parameter buf
12+
| Then, it was used here
13+
814
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 ---------------------------------------------------
15+
Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
16+
and therefore is no longer available.
17+
18+
where: ^ refers to a fresh root capability in the type of value buf1
19+
18 | if ??? then buf1.append(2) // OK
20+
| ----
21+
| The capability was consumed here.
22+
19 | else buf1.append(3) // OK
923
20 | val buf3 = buf1.append(4) // error
1024
| ^^^^
11-
|Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
12-
|on line 18 and therefore is no longer available.
13-
|
14-
|where: ^ refers to a fresh root capability in the type of value buf1
25+
| Then, it was used here
26+
1527
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 ---------------------------------------------------
28+
Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
29+
and therefore is no longer available.
30+
31+
where: ^ refers to a fresh root capability in the type of value buf1
32+
25 | case 1 => buf1.append(2) // OK
33+
| ----
34+
| The capability was consumed here.
35+
26 | case 2 => buf1.append(2)
36+
27 | case _ => buf1.append(3)
1637
28 | val buf3 = buf1.append(4) // error
1738
| ^^^^
18-
|Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
19-
|on line 25 and therefore is no longer available.
20-
|
21-
|where: ^ refers to a fresh root capability in the type of value buf1
39+
| Then, it was used here
40+
2241
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 ---------------------------------------------------
42+
Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
43+
and therefore is no longer available.
44+
45+
where: ^ refers to a fresh root capability in the type of value buf1
46+
33 | case 1 => buf1.append(2) // OK
47+
| ----
48+
| The capability was consumed here.
49+
34 | case 2 => buf1.append(2)
50+
35 | case 3 => buf1.append(3)
51+
36 | case 4 => buf1.append(4)
52+
37 | case 5 => buf1.append(5)
2353
38 | val buf3 = buf1.append(4) // error
2454
| ^^^^
25-
|Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
26-
|on line 33 and therefore is no longer available.
27-
|
28-
|where: ^ refers to a fresh root capability in the type of value buf1
55+
| Then, it was used here
56+
2957
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ----------------------------------------------------
3058
42 | buf.append(1) // error
3159
| ^^^

‎tests/neg-custom-args/captures/linear-buffer.check‎

Lines changed: 53 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -34,33 +34,61 @@
3434
| Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
3535
| The access must be in a consume method to allow this.
3636
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:23:17 -----------------------------------------------------
37+
Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app
38+
and therefore is no longer available.
39+
40+
where: ^ refers to a fresh root capability in the type of parameter buf
41+
21 | val buf1: Buffer[Int]^ = app(buf, 1)
42+
| ---
43+
| The capability was consumed here.
44+
22 | val buf2 = app(buf1, 2) // OK
3745
23 | val buf3 = app(buf, 3) // error
3846
| ^^^
39-
|Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app
40-
|on line 21 and therefore is no longer available.
41-
|
42-
|where: ^ refers to a fresh root capability in the type of parameter buf
47+
| Then, it was used here
48+
4349
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 -----------------------------------------------------
50+
Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
51+
and therefore is no longer available.
52+
53+
where: ^ refers to a fresh root capability in the type of value buf1
54+
28 | if ??? then app(buf1, 2) // OK
55+
| ----
56+
| The capability was consumed here.
57+
29 | else app(buf1, 3) // OK
4458
30 | val buf3 = app(buf1, 4) // error
4559
| ^^^^
46-
|Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
47-
|on line 28 and therefore is no longer available.
48-
|
49-
|where: ^ refers to a fresh root capability in the type of value buf1
60+
| Then, it was used here
61+
5062
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 -----------------------------------------------------
63+
Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
64+
and therefore is no longer available.
65+
66+
where: ^ refers to a fresh root capability in the type of value buf1
67+
35 | case 1 => app(buf1, 2) // OK
68+
| ----
69+
| The capability was consumed here.
70+
36 | case 2 => app(buf1, 2)
71+
37 | case _ => app(buf1, 3)
5172
38 | val buf3 = app(buf1, 4) // error
5273
| ^^^^
53-
|Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
54-
|on line 35 and therefore is no longer available.
55-
|
56-
|where: ^ refers to a fresh root capability in the type of value buf1
74+
| Then, it was used here
75+
5776
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 -----------------------------------------------------
77+
Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
78+
and therefore is no longer available.
79+
80+
where: ^ refers to a fresh root capability in the type of value buf1
81+
43 | case 1 => app(buf1, 2) // OK
82+
| ----
83+
| The capability was consumed here.
84+
44 | case 2 => app(buf1, 2)
85+
45 | case 3 => app(buf1, 3)
86+
46 | case 4 => app(buf1, 4)
87+
47 | case 5 => app(buf1, 5)
5888
48 | val buf3 = app(buf1, 4) // error
5989
| ^^^^
60-
|Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
61-
|on line 43 and therefore is no longer available.
62-
|
63-
|where: ^ refers to a fresh root capability in the type of value buf1
90+
| Then, it was used here
91+
6492
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------
6593
52 | app(buf, 1) // error
6694
| ^^^
@@ -69,7 +97,14 @@
6997
|
7098
| where: ^ refers to a fresh root capability in the type of parameter buf
7199
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:62:20 -----------------------------------------------------
100+
Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app
101+
and therefore is no longer available.
102+
59 | val buf1 = app(buf, "hi") // buf unavailable from here
103+
| ---
104+
| The capability was consumed here.
105+
60 | val c1 = contents(buf1) // only buf.rd is consumed
106+
61 | val c2 = contents(buf1) // buf.rd can be consumed repeatedly
72107
62 | val c3 = contents(buf) // error
73108
| ^^^
74-
| Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app
75-
| on line 59 and therefore is no longer available.
109+
| Then, it was used here
110+

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

Lines changed: 20 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,29 @@
11
-- Error: tests/neg-custom-args/captures/sep-consume.scala:19:2 --------------------------------------------------------
2+
Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
3+
and therefore is no longer available.
4+
5+
where: ^ refers to a fresh root capability in the type of parameter x
6+
18 | val rx: () => Unit = bad(f) // hides x.rd in the resulting `cap`
7+
| -
8+
| The capability was consumed here.
29
19 | x.put(42) // error
310
| ^
4-
| Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
5-
| on line 18 and therefore is no longer available.
6-
|
7-
| where: ^ refers to a fresh root capability in the type of parameter x
11+
| Then, it was used here
12+
813
-- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 -------------------------------------------------------
14+
Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
15+
and therefore is no longer available.
16+
17+
where: ^ refers to a fresh root capability in the type of parameter x
18+
18 | val rx: () => Unit = bad(f) // hides x.rd in the resulting `cap`
19+
| -
20+
| The capability was consumed here.
21+
19 | x.put(42) // error
22+
20 | x.get // ok rd/rd
923
21 | par(rx, () => x.put(42)) // error
1024
| ^
11-
| Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
12-
| on line 18 and therefore is no longer available.
13-
|
14-
| where: ^ refers to a fresh root capability in the type of parameter x
25+
| Then, it was used here
26+
1527
-- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 -------------------------------------------------------
1628
26 | def foo = bad(f) // error
1729
| ^

0 commit comments

Comments
 (0)