|
11 | 11 | -- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 ----------------------------------------------------- |
12 | 12 | 19 | val buf3 = app(buf, 3) // error |
13 | 13 | | ^^^ |
14 | | - | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a |
15 | | - | @consume parameter or was used as a prefix to a @consume method on line 17 |
16 | | - | and therefore is no longer available. |
| 14 | + | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a |
| 15 | + | @consume parameter or was used as a prefix to a @consume method on line 17 |
| 16 | + | and therefore is no longer available. |
17 | 17 | | |
18 | | - | where: ^ refers to a fresh root capability in the type of parameter buf |
| 18 | + | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf |
19 | 19 | -- Error: tests/neg-custom-args/captures/linear-buffer.scala:26:17 ----------------------------------------------------- |
20 | 20 | 26 | val buf3 = app(buf1, 4) // error |
21 | 21 | | ^^^^ |
22 | 22 | | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a |
23 | 23 | | @consume parameter or was used as a prefix to a @consume method on line 24 |
24 | 24 | | and therefore is no longer available. |
25 | 25 | | |
26 | | - | where: ^ refers to a fresh root capability in the type of value buf1 |
| 26 | + | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 |
27 | 27 | -- Error: tests/neg-custom-args/captures/linear-buffer.scala:34:17 ----------------------------------------------------- |
28 | 28 | 34 | val buf3 = app(buf1, 4) // error |
29 | 29 | | ^^^^ |
30 | 30 | | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a |
31 | 31 | | @consume parameter or was used as a prefix to a @consume method on line 31 |
32 | 32 | | and therefore is no longer available. |
33 | 33 | | |
34 | | - | where: ^ refers to a fresh root capability in the type of value buf1 |
| 34 | + | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 |
35 | 35 | -- Error: tests/neg-custom-args/captures/linear-buffer.scala:44:17 ----------------------------------------------------- |
36 | 36 | 44 | val buf3 = app(buf1, 4) // error |
37 | 37 | | ^^^^ |
38 | 38 | | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a |
39 | 39 | | @consume parameter or was used as a prefix to a @consume method on line 39 |
40 | 40 | | and therefore is no longer available. |
41 | 41 | | |
42 | | - | where: ^ refers to a fresh root capability in the type of value buf1 |
| 42 | + | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 |
43 | 43 | -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:8 ------------------------------------------------------ |
44 | 44 | 48 | app(buf, 1) // error |
45 | 45 | | ^^^ |
46 | 46 | | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot |
47 | 47 | | be passed to a @consume parameter or be used as a prefix of a @consume method call. |
48 | 48 | | |
49 | | - | where: ^ refers to a fresh root capability in the type of parameter buf |
| 49 | + | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf |
0 commit comments