#3057. Add return statement in loops tests

TypeSystem/flow-analysis/reachability_do_while_A03_t09.dart

@@ -0,0 +1,28 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion do while statement: If `N` is a do while statement of the form
+/// `do S while (E)` then:
+/// - Let `before(S) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
+/// - Let `before(E) = join(after(S), continue(N))`
+/// - Let `after(N) = join(false(E), break(S))`
+///
+/// @description Checks that `after(N) = join(false(E), break(S))`. Test that an
+/// assignment in `S` after `return` is unreachable.
+/// @author [email protected]
+
+main() {
+  late int i;
+  if (1 > 2) {
+    do {
+      return;
+      i = 42;
+    } while (false);
+    i; // Ok. `after(N)` is unreachable
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}

TypeSystem/flow-analysis/reachability_for_A01_t13.dart

@@ -0,0 +1,48 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion for statement: If `N` is a for statement of the form
+/// `for (D; C; U) S,` then:
+/// - Let `before(D) = before(N)`.
+/// - Let `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`
+/// - Let `before(S) = split(true(C))`.
+/// - Let `before(U) = merge(after(S), continue(S))`.
+/// - Let `after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U))`
+///
+/// @description Checks that
+/// `before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N))`. Test
+/// that an assignment in `S` after `return` is unreachable.
+/// @author [email protected]
+
+test1() {
+  late int i;
+  if (2 < 1) {
+    for (;;) {
+      return;
+      i = 42;
+    }
+    i; // Ok. `after(N)` is unreachable
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+test2() {
+  late int i;
+  if (2 < 1) {
+    for (int j = 0; j < 1;) {
+      return;
+      i = 42;
+    }
+    i; // Ok. `after(N)` is unreachable
+  }
+  i; // Possibly assigned
+}
+
+main() {
+  print(test1);
+  print(test2);
+}

TypeSystem/flow-analysis/reachability_for_in_A02_t08.dart

@@ -0,0 +1,31 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion for each statement: If `N` is a for statement of the form
+/// `for (T X in E) S`, `for (var X in E) S`, or `for (X in E) S`, then:
+/// - Let `before(E) = before(N)`
+/// - Let `before(S) = conservativeJoin(after(E), assignedIn(N), capturedIn(N))`
+/// - Let `after(N) = join(before(S), break(S))`
+///
+/// @description Checks that
+/// `before(S) = conservativeJoin(after(E), assignedIn(N), capturedIn(N))`. Test
+/// that if there is an assignment in `S` (even after the `return` statement)
+/// then in `after(N)` the variable is "possibly assigned".
+/// @author [email protected]
+
+test() {
+  late int i;
+  if (2 > 1) {
+    for (var j in []) {
+      return;
+      i = 42;
+    }
+    i; // Possibly assigned. See https://github.com/dart-lang/sdk/issues/42232#issuecomment-690681385
+  }
+  i; // Possibly assigned
+}
+
+main() {
+  print(test);
+}

TypeSystem/flow-analysis/reachability_while_A01_t04.dart

@@ -0,0 +1,47 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion while statement: If `N` is a while statement of the form
+/// `while (E) S` then:
+/// - Let `before(E) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`
+/// - Let `before(S) = split(true(E))`.
+/// - Let `after(N) = inheritTested(join(false(E), unsplit(break(S))), after(S))`
+///
+/// @description Checks that
+/// `before(E) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`.
+/// Test if there is an assignment in `S` (even after the `return` statement)
+/// then `after(N)` the variable is "possibly assigned".
+/// @author [email protected]
+
+test1() {
+  late int i;
+  if (1 > 2) {
+    while (2 > 1) {
+      return;
+      i = 42;
+    }
+    i; // Possibly assigned. See https://github.com/dart-lang/sdk/issues/42232#issuecomment-690681385
+  }
+  i; // Possibly assigned.
+}
+
+test2() {
+  late int i;
+  if (1 > 2) {
+    while (true) {
+      return;
+      i = 42;
+    }
+    i; // Possibly assigned and dead code
+  }
+  i; // Definitely unassigned.
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test1);
+  print(test2);
+}

TypeSystem/flow-analysis/reachability_while_A03_t01.dart

@@ -8,11 +8,11 @@
 /// - Let `before(S) = split(true(E))`.
 /// - Let `after(N) = inheritTested(join(false(E), unsplit(break(S))), after(S))`
 ///
-/// @description Checks that if `E` is not a boolean literal flow analysis
-/// detects assignment in `S`.
+/// @description Checks that if `E` is a boolean `true` literal and there is no
+/// reachable `break` in `S` then `after(N) is unreachable.
 /// @author [email protected]
 
-main() {
+test1() {
   late int i;
   if (1 > 2) {
     while (true) {
@@ -27,3 +27,38 @@ main() {
 // [analyzer] unspecified
 // [cfe] unspecified
 }
+
+test2() {
+  late int i;
+  if (1 > 2) {
+    while (true) {
+      if (false) {
+        return;
+      }
+    }
+    i = 42;
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+test3() {
+  late int i;
+  if (1 > 2) {
+    while (true) {
+      return;
+    }
+    i = 42;
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test1);
+  print(test2);
+}

TypeSystem/flow-analysis/reachability_while_A03_t02.dart

@@ -0,0 +1,27 @@
+// Copyright (c) 2025, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+/// @assertion while statement: If `N` is a while statement of the form
+/// `while (E) S` then:
+/// - Let `before(E) = conservativeJoin(before(N), assignedIn(N), capturedIn(N))`
+/// - Let `before(S) = split(true(E))`.
+/// - Let `after(N) = inheritTested(join(false(E), unsplit(break(S))), after(S))`
+///
+/// @description Checks that if `E` is a boolean `true` literal and there is no
+/// reachable `break` in `S` then `after(N)` is unreachable.
+/// @author [email protected]
+
+main() {
+  late int i;
+  if (1 > 2) {
+    while (true) {
+      continue;
+    }
+    i = 42; // Dead code
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}