File tree Expand file tree Collapse file tree 5 files changed +87
-57
lines changed Expand file tree Collapse file tree 5 files changed +87
-57
lines changed Original file line number Diff line number Diff line change 1+ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:15:4 ----------------------------------
2+ 14 | val (a, b) = freeze:
3+ 15 | val t1 = allocRef() // error
4+ | ^
5+ | Capability cap outlives its scope: it leaks into outer capture set 's1 which is owned by value x1.
6+ | The leakage occurred when trying to match the following types:
7+ |
8+ | Found: (Ref^{cap}, Ref^{cap²})^'s2
9+ | Required: (Ref^'s1, Ref^'s3)^'s4
10+ |
11+ | where: cap and cap² refer to a root capability associated with the result type of (): (Ref^, Ref^²)^'s2
12+ 16 | val t2 = allocRef()
13+ 17 | (t1, t2)
14+ |
15+ | longer explanation available when compiling with `-explain`
16+ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:22:16 ---------------------------------
17+ 22 | val (a: Ref^{}, b: Ref^{}) = freeze: // error // error
18+ | ^
19+ | Found: Ref^{a0.rd}
20+ | Required: Ref^{}
21+ |
22+ | Note that capability a0.rd is not included in capture set {}.
23+ |
24+ | longer explanation available when compiling with `-explain`
25+ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze-tuple.scala:22:27 ---------------------------------
26+ 22 | val (a: Ref^{}, b: Ref^{}) = freeze: // error // error
27+ | ^
28+ | Found: Ref^{b0.rd}
29+ | Required: Ref^{}
30+ |
31+ | Note that capability b0.rd is not included in capture set {}.
32+ |
33+ | longer explanation available when compiling with `-explain`
Original file line number Diff line number Diff line change 1+ import language .experimental .captureChecking
2+ import language .experimental .separationChecking
3+ import caps .{Mutable , freeze }
4+
5+ // A mutable ref and its immutable version
6+ class Ref extends Mutable :
7+ private var data : Int = 0
8+ def get : Int = data
9+ update def set (x : Int ): Unit = data = x
10+ def allocRef (): Ref ^ = Ref ()
11+ type IRef = Ref ^ {}
12+
13+ def test1 (): Unit =
14+ val (a, b) = freeze :
15+ val t1 = allocRef() // error
16+ val t2 = allocRef()
17+ (t1, t2)
18+
19+ def test2 (): Unit =
20+ val a0 = allocRef()
21+ val b0 = allocRef()
22+ val (a : Ref ^ {}, b : Ref ^ {}) = freeze : // error // error
23+ (a0, b0)
Original file line number Diff line number Diff line change 1- -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:13:17 ---------------------------------------
2- 13 | val b = freeze(a) // error
3- | ^
4- | Found: () ?->{a} Arr[String]^{a}
5- | Required: () ?-> <?>
1+ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:19:4 ----------------------------------------
2+ 18 | val a2 = freeze:
3+ 19 | val a = Arr[String](2) // error
4+ | ^
5+ |Capability cap outlives its scope: it leaks into outer capture set 's1 of value a2.
6+ |The leakage occurred when trying to match the following types:
67 |
7- | Note that capability a is not included in capture set {}.
8+ |Found: (Arr[String]^{cap}, Arr[String]^{cap²})^'s2
9+ |Required: (Arr[String]^'s1, Arr[String]^'s3)^'s4
810 |
9- | longer explanation available when compiling with `-explain`
10- -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/freeze.scala:22:4 ----------------------------------------
11- 21 | freeze:
12- 22 | mkExclusive() // error
13- | ^
14- | Capability cap outlives its scope: it leaks into outer capture set 's1 of method test3.
15- | The leakage occurred when trying to match the following types:
16- |
17- | Found: EX^{cap}
18- | Required: EX^'s1
19- |
20- | where: cap is a root capability associated with the result type of (): EX^
11+ |where: cap and cap² refer to a root capability associated with the result type of (): (Arr[String]^, Arr[String]^²)^'s2
12+ 20 | val b = Arr[String](2)
13+ 21 | a(0) = "1"
14+ 22 | a(1) = "2"
15+ 23 | b(0) = "1"
16+ 24 | b(1) = "2"
17+ 25 | (a, b)
2118 |
2219 | longer explanation available when compiling with `-explain`
Original file line number Diff line number Diff line change 1+ import language .experimental .captureChecking
12import caps .*
23
34class Arr [T : reflect.ClassTag ](len : Int ) extends Mutable :
@@ -7,17 +8,19 @@ class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
78
89
910def test2 =
10- val a = Arr [String ](2 )
11- a(0 ) = " 1"
12- a(1 ) = " 2"
13- val b = freeze(a) // error
14- b
15-
16- class EX
17-
18- def mkExclusive (): EX ^ = ???
19-
20- def test3 =
21- freeze :
22- mkExclusive() // error
11+ val a = freeze :
12+ val a = Arr [String ](2 )
13+ a(0 ) = " 1"
14+ a(1 ) = " 2"
15+ a
16+ val _: Arr [String ]^ {} = a
2317
18+ val a2 = freeze :
19+ val a = Arr [String ](2 ) // error
20+ val b = Arr [String ](2 )
21+ a(0 ) = " 1"
22+ a(1 ) = " 2"
23+ b(0 ) = " 1"
24+ b(1 ) = " 2"
25+ (a, b)
26+ val _: (Arr [String ]^ {}, Arr [String ]^ {}) = a2
Load Diff This file was deleted.
You can’t perform that action at this time.
0 commit comments