|
7 | 7 | |where: => refers to a fresh root capability created in method runAll0 when checking argument to parameter f of method usingFile
|
8 | 8 | | ^ refers to the universal root capability
|
9 | 9 | |
|
10 |
| - |Note that capability cap is not included in capture set {xs*}. |
| 10 | + |Note that capability cap is not included in capture set {C}. |
11 | 11 | 23 | cur = (() => f.write()) :: Nil
|
12 | 12 | |
|
13 | 13 | | longer explanation available when compiling with `-explain`
|
|
20 | 20 | |where: => refers to a fresh root capability created in method runAll1 when checking argument to parameter f of method usingFile
|
21 | 21 | | ^ refers to the universal root capability
|
22 | 22 | |
|
23 |
| - |Note that capability cap cannot be included in capture set {xs*} of value cur. |
| 23 | + |Note that capability cap cannot be included in capture set {C} of value cur. |
24 | 24 | 33 | cur.set:
|
25 | 25 | 34 | (() => f.write()) :: Nil
|
26 | 26 | |
|
|
125 | 125 | |where: => refers to a fresh root capability created in method mapCompose2 when checking argument to parameter f of method map
|
126 | 126 | | ^ refers to the universal root capability
|
127 | 127 | |
|
128 |
| - |Note that capability ps* cannot be included in capture set {} of value x. |
| 128 | + |Note that capability C cannot be included in capture set {} of value x. |
129 | 129 | |
|
130 | 130 | | longer explanation available when compiling with `-explain`
|
131 | 131 | -- Error: tests/neg-custom-args/captures/reaches.scala:39:31 -----------------------------------------------------------
|
132 | 132 | 39 | val next: () => Unit = cur.head // error
|
133 | 133 | | ^^^^^^^^
|
134 | 134 | | Local reach capability xs* leaks into capture scope of method runAll2.
|
135 |
| - | To allow this, the parameter xs should be declared with a @use annotation |
| 135 | + | You could try to abstract the capabilities referred to by xs* in a capset variable. |
136 | 136 | -- Error: tests/neg-custom-args/captures/reaches.scala:62:36 -----------------------------------------------------------
|
137 | 137 | 62 | val leaked = usingFile[File^{id*}]: f => // error: separation
|
138 | 138 | | ^
|
139 |
| - | Separation failure: Illegal access to cap of value id which is hidden by the previous definition |
140 |
| - | of value id with type File^ -> File^². |
141 |
| - | This type hides capabilities {cap} |
| 139 | + | Local cap created in type of parameter x leaks into capture scope of enclosing function |
142 | 140 | |
|
143 |
| - | where: ^ refers to the universal root capability |
144 |
| - | ^² refers to a fresh root capability in the type of value id |
145 |
| - | cap is a fresh root capability created in value id |
| 141 | + | where: cap is a fresh root capability created in value id of parameter parameter x of method $anonfun |
146 | 142 | 63 | val f1: File^{id*} = id(f)
|
147 | 143 | 64 | f1
|
0 commit comments