File tree Expand file tree Collapse file tree 2 files changed +34
-0
lines changed
tests/neg-custom-args/captures Expand file tree Collapse file tree 2 files changed +34
-0
lines changed Original file line number Diff line number Diff line change 1+ -- Error: tests/neg-custom-args/captures/boxed-consume.scala:10:52 -----------------------------------------------------
2+ 10 | def h(consume x: (Object^, Object^)): Object^ = x._1 // error: local reach leak
3+ | ^^^^
4+ | Local reach capability x._1* leaks into capture scope of method h.
5+ | You could try to abstract the capabilities referred to by x._1* in a capset variable.
6+ -- Error: tests/neg-custom-args/captures/boxed-consume.scala:16:10 -----------------------------------------------------
7+ 16 | println(d) // error
8+ | ^
9+ | Separation failure: Illegal access to (d : Object^), which was passed as a consume parameter to method g
10+ | on line 15 and therefore is no longer available.
11+ |
12+ | where: ^ refers to a fresh root capability in the type of value d
Original file line number Diff line number Diff line change 1+ import caps .*
2+
3+ def Test =
4+ val c : Object ^ = " a"
5+ val d : Object ^ = " a"
6+ val e1, e2 : Object ^ = " a"
7+ val falseDeps : Object ^ = " a"
8+ def f [T ](consume x : T ): Unit = ()
9+ def g (consume x : Object ^ ): Unit = ()
10+ def h (consume x : (Object ^ , Object ^ )): Object ^ = x._1 // error: local reach leak
11+ val cc = (c, c)
12+ f(cc) // no consume, it's boxed
13+ f(c) // no consume, it's boxed
14+ println(c) // ok
15+ g(d) // consume
16+ println(d) // error
17+ h((e1, e2)) // no consume, still boxed
18+ println(e1) // ok
19+
20+
21+
22+
You can’t perform that action at this time.
0 commit comments