Skip to content

Commit 3f197e0

Browse files
sgrekhovsgrekhov
authored
#3057. Add tests for the reachability of a do-while loop. (#3112)
Add tests for the reachability of a do-while loop.
1 parent 7e4321a commit 3f197e0

19 files changed

+491
-8
lines changed

‎TypeSystem/flow-analysis/definite_assignment_A06_t01.dart

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,13 @@
22
// for details. All rights reserved. Use of this source code is governed by a
33
// BSD-style license that can be found in the LICENSE file.
44

5-
/// @assertion assigned is a boolean value indicating whether the variable has
6-
/// definitely been assigned at the given point in the source code. When assigned
7-
/// is true, we say that the variable is definitely assigned at that point.
5+
/// @assertion `assigned` is a boolean value indicating whether the variable has
6+
/// definitely been assigned at the given point in the source code. When
7+
/// `assigned` is true, we say that the variable is definitely assigned at that
8+
/// point.
89
///
9-
/// @description Checks definite assignment and do-while loop
10+
/// @description Checks that an assignment in the body of a do-while loop is a
11+
/// definite assignment.
1012
/// @author [email protected]
1113
1214
main() {

‎TypeSystem/flow-analysis/definite_assignment_A06_t02.dart

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,13 @@
22
// for details. All rights reserved. Use of this source code is governed by a
33
// BSD-style license that can be found in the LICENSE file.
44

5-
/// @assertion assigned is a boolean value indicating whether the variable has
6-
/// definitely been assigned at the given point in the source code. When assigned
7-
/// is true, we say that the variable is definitely assigned at that point.
5+
/// @assertion `assigned` is a boolean value indicating whether the variable has
6+
/// definitely been assigned at the given point in the source code. When
7+
/// `assigned` is true, we say that the variable is definitely assigned at that
8+
/// point.
89
///
9-
/// @description Checks definite assignment and do-while loop
10+
/// @description Checks that an assignment in the condition part of a do-while
11+
/// loop with an empty body is a definite assignment.
1012
/// @author [email protected]
1113
1214
main() {

‎TypeSystem/flow-analysis/reachability_do_while_A01_t01.dart

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that if a variable is assigned in `S` then it is not
12+
/// definitely unassigned in `S`.
13+
/// @author [email protected]
14+
15+
main() {
16+
late int i;
17+
do {
18+
if (1 > 2) {
19+
i; // Not definitely unassigned
20+
};
21+
i = 42;
22+
} while (false);
23+
}

‎TypeSystem/flow-analysis/reachability_do_while_A01_t02.dart

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that if a variable is assigned in `S` then it is not
12+
/// definitely unassigned in `E`.
13+
/// @author [email protected]
14+
15+
main() {
16+
late int i;
17+
do {
18+
i = 42;
19+
} while (i < 0);
20+
}

‎TypeSystem/flow-analysis/reachability_do_while_A01_t03.dart

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that if a variable is captured in `S` then it is
12+
/// detected by flow analysis of `S`.
13+
/// @author [email protected]
14+
15+
test1(int? n) {
16+
if (n != null) { // promoted to `int`
17+
do {
18+
() {
19+
n = 42; // demoted to `int?`
20+
};
21+
n.isEven;
22+
// ^^^^^^
23+
// [analyzer] unspecified
24+
// [cfe] unspecified
25+
} while (false);
26+
}
27+
}
28+
29+
test2(int? n) {
30+
if (n != null) { // promoted to `int`
31+
do {
32+
n.isEven;
33+
// ^^^^^^
34+
// [analyzer] unspecified
35+
// [cfe] unspecified
36+
late int i = (n = 42); // demoted to `int?`
37+
} while (false);
38+
}
39+
}
40+
41+
main() {
42+
print(test1);
43+
print(test2);
44+
}

‎TypeSystem/flow-analysis/reachability_do_while_A01_t04.dart

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that if a variable is captured in `S` then it is
12+
/// detected by flow analysis of `E`.
13+
/// @author [email protected]
14+
15+
test(int? n) {
16+
if (n != null) { // promoted to `int`
17+
do {
18+
() {
19+
n = 42; // demoted to `int?`
20+
};
21+
} while (n > 0);
22+
// ^
23+
// [analyzer] unspecified
24+
// [cfe] unspecified
25+
}
26+
}
27+
28+
main() {
29+
print(test);
30+
}

‎TypeSystem/flow-analysis/reachability_do_while_A01_t05.dart

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that `capturedIn(E)` is detected by flow analysis.
12+
/// @author [email protected]
13+
14+
test1(int? n) {
15+
if (n != null) { // n promoted to `int`
16+
do {
17+
n.isEven;
18+
// ^^^^^^
19+
// [analyzer] unspecified
20+
// [cfe] unspecified
21+
} while ((() => (n = 42) < 0)()); // n demoted to `int?`
22+
}
23+
}
24+
25+
test2(int? n) {
26+
if (n != null) { // n promoted to `int`
27+
do {
28+
} while ((() => (n = 42) < 0)()); // n demoted to `int?`
29+
n.isEven;
30+
// ^^^^^^
31+
// [analyzer] unspecified
32+
// [cfe] unspecified
33+
}
34+
}
35+
36+
main() {
37+
print(test1);
38+
print(test2);
39+
}

‎TypeSystem/flow-analysis/reachability_do_while_A02_t01.dart

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that `before(E) = join(after(S), continue(N))`. Test
12+
/// that if `S` throws then `E` is unreachable.
13+
/// @author [email protected]
14+
15+
test(Never n) {
16+
late int i;
17+
if (1 > 2) {
18+
do {
19+
n;
20+
} while ((i = 42) < 0);
21+
}
22+
i; // Definitely unassigned
23+
//^
24+
// [analyzer] unspecified
25+
// [cfe] unspecified
26+
}
27+
28+
main() {
29+
print(test);
30+
}

‎TypeSystem/flow-analysis/reachability_do_while_A02_t02.dart

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that `before(E) = join(after(S), continue(N))`. Test
12+
/// that if `S` breaks then an assignment in `E` is treated as
13+
/// 'possibly assigned'.
14+
/// @author [email protected]
15+
/// @issue 60361
16+
17+
main() {
18+
late int i;
19+
do {
20+
break;
21+
} while ((i = 42) < 0); // Possibly assigned. https://github.com/dart-lang/sdk/issues/42232#issuecomment-690681385
22+
i; // Not definitely unassigned
23+
}

‎TypeSystem/flow-analysis/reachability_do_while_A02_t03.dart

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
// Copyright (c) 2025, the Dart project authors. Please see the AUTHORS file
2+
// for details. All rights reserved. Use of this source code is governed by a
3+
// BSD-style license that can be found in the LICENSE file.
4+
5+
/// @assertion do while statement: If `N` is a do while statement of the form
6+
/// `do S while (E)` then:
7+
/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
8+
/// - Let `before(E) = join(after(S), continue(N))`
9+
/// - Let `after(N) = join(false(E), break(S))`
10+
///
11+
/// @description Checks that `before(E) = join(after(S), continue(N))`. Test
12+
/// that if `S` has a `return` then an assignment in `E` will never happen.
13+
/// @author [email protected]
14+
15+
main() {
16+
late int i;
17+
if (1 > 2) {
18+
do {
19+
return;
20+
} while ((i = 42) < 0);
21+
}
22+
i; // Definitely unassigned
23+
//^
24+
// [analyzer] unspecified
25+
// [cfe] unspecified
26+
}

0 commit comments

Comments
 (0)