#3057. Add while statements tests and update assignments (#3107)

Add while statements tests and update assignments

Author: sgrekhov

TypeSystem/flow-analysis/definite_assignment_A05_t01.dart

@@ -2,11 +2,14 @@
 // 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 assigned is a boolean value indicating whether the variable has
-/// definitely been assigned at the given point in the source code. When assigned
-/// is true, we say that the variable is definitely assigned at that point.
+/// @assertion `assigned` is a boolean value indicating whether the variable has
+/// definitely been assigned at the given point in the source code. When
+/// `assigned` is true, we say that the variable is definitely assigned at that
+/// point.
 ///
-/// @description Checks definite assignment and while loop
+/// @description Checks that if the condition of a `while` statement is not the
+/// `true` literal, then an assignment in the body of the loop is not treated by
+/// flow analysis as a definite assignment.
 /// @author [email protected]
 
 main() {

TypeSystem/flow-analysis/definite_assignment_A05_t02.dart

@@ -2,11 +2,14 @@
 // 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 assigned is a boolean value indicating whether the variable has
-/// definitely been assigned at the given point in the source code. When assigned
-/// is true, we say that the variable is definitely assigned at that point.
+/// @assertion `assigned` is a boolean value indicating whether the variable has
+/// definitely been assigned at the given point in the source code. When
+/// `assigned` is true, we say that the variable is definitely assigned at that
+/// point.
 ///
-/// @description Checks definite assignment and while loop
+/// @description Checks that if the condition of a `while` statement is the
+/// `true` literal, then an assignment in the body of the loop is treated by
+/// flow analysis as a definite assignment.
 /// @author [email protected]
 
 main() {

TypeSystem/flow-analysis/definite_assignment_A05_t03.dart

@@ -2,15 +2,19 @@
 // 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 assigned is a boolean value indicating whether the variable has
-/// definitely been assigned at the given point in the source code. When assigned
-/// is true, we say that the variable is definitely assigned at that point.
+/// @assertion `assigned` is a boolean value indicating whether the variable has
+/// definitely been assigned at the given point in the source code. When
+/// `assigned` is true, we say that the variable is definitely assigned at that
+/// point.
 ///
-/// @description Checks definite assignment and while loop
+/// @description Checks that if the condition of a `while` statement is the
+/// `false` literal, then an assignment in the body of the loop is treated by
+/// flow analysis as a definite unassignment.
 /// @author [email protected]
+/// @issue 60322
 
 main() {
-  int n;
+  late int n;
   while (false) {
     n = 42;
   }

TypeSystem/flow-analysis/definite_assignment_A05_t04.dart

@@ -2,11 +2,13 @@
 // 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 assigned is a boolean value indicating whether the variable has
-/// definitely been assigned at the given point in the source code. When assigned
-/// is true, we say that the variable is definitely assigned at that point.
+/// @assertion `assigned` is a boolean value indicating whether the variable has
+/// definitely been assigned at the given point in the source code. When
+/// `assigned` is true, we say that the variable is definitely assigned at that
+/// point.
 ///
-/// @description Checks definite assignment and while loop
+/// @description Checks that an assignment in the condition of a `while`
+/// statement is the is treated by flow analysis as a definite assignment.
 /// @author [email protected]
 
 main() {

TypeSystem/flow-analysis/promotion_via_assignment_A01_t01.dart

@@ -12,7 +12,7 @@
 ///  and T <: S and not S <: T
 ///  and T is a type of interest for x in tested
 ///
-/// @description Checks that a variable is promotable to the type T if all
+/// @description Checks that a variable is promotable to the type `T` if all
 /// requirements above are met.
 /// @author [email protected]
 
@@ -23,9 +23,7 @@ class T extends S {
 
 main() {
   S x = new S();
-  if (x is T) {
-    // nothing
-  }
+  if (x is T) {}  // make `T` a type of interest
   x = new T();
   x.foo();
 }

TypeSystem/flow-analysis/promotion_via_assignment_A02_t01.dart

@@ -12,8 +12,8 @@
 ///  and T <: S and not S <: T
 ///  and T is a type of interest for x in tested
 ///
-/// @description Checks that if captured is true then promotion via assignment is
-/// not performed
+/// @description Checks that if `captured` is `true` then promotion via
+/// assignment is not performed
 /// @author [email protected]
 
 class S {}
@@ -29,9 +29,7 @@ main() {
     x = v;
   }
   f = bar;
-  if (x is T) {
-    // nothing
-  }
+  if (x is T) {} // make `T` a type of interest
   x = new T();
   x.foo();
 //  ^^^

TypeSystem/flow-analysis/promotion_via_assignment_A03_t01.dart

@@ -12,8 +12,8 @@
 ///  and T <: S and not S <: T
 ///  and T is a type of interest for x in tested
 ///
-/// @description Checks that if T <: S and S <: T then promotion via assignment
-/// is not performed
+/// @description Checks that if `T <: S` and `S <: T` then promotion via
+/// assignment is not performed
 /// @author [email protected]
 
 import '../../Utils/expect.dart';
@@ -25,9 +25,7 @@ class T extends S {
 
 main() {
   dynamic x = new S();
-  if (x is T) {
-    // nothing
-  }
+  if (x is T) {} // make `T` a type of interest
   x = new T();
   x.foo();
   Expect.throws(() {

TypeSystem/flow-analysis/promotion_via_assignment_A04_t01.dart

@@ -12,8 +12,8 @@
 ///  and T <: S and not S <: T
 ///  and T is a type of interest for x in tested
 ///
-/// @description Checks that if T is a type of interest for x in tested then
-/// promotion via assignment is not performed
+/// @description Checks that if `T` is not a type of interest for `x` in
+/// `tested` then promotion via assignment is not performed.
 /// @author [email protected]
 
 class S {}

TypeSystem/flow-analysis/reachability_while_A01_t01.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 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 the static type of `E` is `Never` then `S` is
+/// dead code.
+/// @author [email protected]
+
+Never foo() => throw "Never";
+
+main() {
+  late int i;
+  if (2 > 1) {
+    while (foo()) {
+      i = 42; // Assigned in dead code
+    }
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}

TypeSystem/flow-analysis/reachability_while_A01_t02.dart

@@ -0,0 +1,29 @@
+// 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 the static type of `E` is `Never` then
+/// `after(N)` is dead code.
+/// @author [email protected]
+
+Never foo() => throw "Never";
+
+main() {
+  late int i;
+  if (2 > 1) {
+    while (foo()) {
+      break;
+    }
+    i = 42; // Assigned in dead code
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}