|
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