#3057. Add more flow analysis tests for type Never

TypeSystem/flow-analysis/reachability_A01_t01.dart

@@ -2,21 +2,16 @@
 // 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 Variable or getter: If N is an expression of the form x where the
-/// type of x is T then:
+/// @assertion
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
 ///
-/// If T <: Never then:
-///  Let null(N) = unreachable(before(N)).
-///  Let notNull(N) = unreachable(before(N)).
-/// Otherwise if T <: Null then:
-///  Let null(N) = before(N).
-///  Let notNull(N) = unreachable(before(N)).
-/// Otherwise if T is non-nullable then:
-///  Let null(N) = unreachable(before(N)).
-///  Let notNull(N) = before(N).
-///
-/// @description Checks reachability after variable or getter. Test variable of
-/// type Never
+/// @description Checks that the code is unreachable after a variable of type
+/// `Never`.
 /// @author sgrekhov@unipro.ru
 
 void test(Never n) {
@@ -35,6 +30,5 @@ void test(Never n) {
 main() {
   try {
     test(throw "Lily was here");
-  } catch (_) {
-  }
+  } catch (_) {}
 }

TypeSystem/flow-analysis/reachability_A01_t02.dart

@@ -2,21 +2,16 @@
 // 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 Variable or getter: If N is an expression of the form x where the
-/// type of x is T then:
+/// @assertion
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
 ///
-/// If T <: Never then:
-///  Let null(N) = unreachable(before(N)).
-///  Let notNull(N) = unreachable(before(N)).
-/// Otherwise if T <: Null then:
-///  Let null(N) = before(N).
-///  Let notNull(N) = unreachable(before(N)).
-/// Otherwise if T is non-nullable then:
-///  Let null(N) = unreachable(before(N)).
-///  Let notNull(N) = before(N).
-///
-/// @description Checks reachability after variable or getter. Test getter of
-/// type Never
+/// @description Checks that the code is unreachable after the invocation of a
+/// getter of type `Never`.
 /// @author sgrekhov@unipro.ru
 
 Never get n => throw "Lily was here";
@@ -30,7 +25,7 @@ main() {
       i = 42;   // Variable is initialized in a dead code. This leaves it definitely unassigned
     }
     i; // It is an error to read a local late variable when it is definitely unassigned.
-//^
+//  ^
 // [analyzer] unspecified
 // [cfe] unspecified
   } catch (_) {}

TypeSystem/flow-analysis/reachability_A01_t11.dart

@@ -0,0 +1,34 @@
+// 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
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
+///
+/// @description Checks that the code is unreachable after a variable of type
+/// `T <: Never`.
+/// @author sgrekhov22@gmail.com
+
+void test<T extends Never>(T n) {
+  late int i;
+  bool b = (() => true)();
+  if (b) {
+    n;        // The code after this point is unreachable
+    i = 42;   // Variable is initialized in a dead code. This leaves it definitely unassigned
+  }
+  i; // It is an error to read a local late variable when it is definitely unassigned.
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  try {
+    test(throw "Lily was here");
+  } catch (_) {}
+}

TypeSystem/flow-analysis/reachability_A01_t12.dart

@@ -0,0 +1,38 @@
+// 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
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
+///
+/// @description Checks that the code is unreachable after the invocation of a
+/// getter of type `T <: Never`.
+/// @author sgrekhov22@gmail.com
+
+class C<T extends Never> {
+  T get n => throw "Lily was here";
+
+  test() {
+    try {
+      late int i;
+      bool b = (() => true)();
+      if (b) {
+        n; // The code after this point is unreachable
+        i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned
+      }
+      i; // It is an error to read a local late variable when it is definitely unassigned.
+//    ^
+// [analyzer] unspecified
+// [cfe] unspecified
+    } catch (_) {}
+  }
+}
+
+main() {
+  print(C);
+}

TypeSystem/flow-analysis/reachability_A01_t13.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
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
+///
+/// @description Checks whether the code is reachable after a variable of a type
+/// other than `T <: Never`.
+/// @author sgrekhov22@gmail.com
+
+void test<T extends Never?>(T n) {
+  late int i;
+  bool b = (() => true)();
+  if (b) {
+    n;
+    i = 42;
+  }
+  i; // Not an error
+}
+
+main() {
+  test(null);
+}

TypeSystem/flow-analysis/reachability_A01_t14.dart

@@ -0,0 +1,35 @@
+// 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
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
+///
+/// @description Checks whether the code is reachable after invocation of a
+/// getter whose type is other than `T <: Never`.
+/// @author sgrekhov22@gmail.com
+
+class C<T extends Never?> {
+  T get n => throw "Lily was here";
+
+  test() {
+    try {
+      late int i;
+      bool b = (() => true)();
+      if (b) {
+        n;
+        i = 42;
+      }
+      i; // Not an error
+    } catch (_) {}
+  }
+}
+
+main() {
+  print(C);
+}

TypeSystem/flow-analysis/reachability_A01_t15.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
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
+///
+/// @description Checks whether the code is reachable after a variable of a type
+/// other that `Never`.
+/// @author sgrekhov22@gmail.com
+
+void test(Never? n) {
+  late int i;
+  bool b = (() => true)();
+  if (b) {
+    n;
+    i = 42;
+  }
+  i; // Not an error
+}
+
+main() {
+  test(null);
+}

TypeSystem/flow-analysis/reachability_A01_t16.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
+/// - Variable or getter: If `N` is an expression of the form `x` where the
+///   type of `x` is `T` then:
+/// If `T <: Never` then:
+///   - Let `after(N) = unreachable(before(N))`.
+/// Otherwise:
+///   - Let `after(N) = before(N)`.
+///
+/// @description Checks whether the code is reachable after invocation of a
+/// getter whose type is other than `Never`.
+/// @author sgrekhov22@gmail.com
+
+import 'dart:async';
+
+FutureOr<Never> get n => 2 > 1 ? throw 1: Future.value(throw 2);
+
+main() {
+  try {
+    late int i;
+    bool b = (() => true)();
+    if (b) {
+      n;
+      i = 42;
+    }
+    i; // Not an error
+  } catch (_) {}
+}