#3057. Add tests for method invocation (#3083)

* #3057. Add tests for method invocation

* Minor code improvement

* Minor code-style changes

* Add async function case

* Apply review suggestions

* Apply review suggestions, iteration #2.

Author: sgrekhov

TypeSystem/flow-analysis/reachability_A22_t01.dart

@@ -0,0 +1,33 @@
+// 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 - Method invocation: If `N` is an expression of the form
+/// `E1.m1(E2)`, then:
+/// - Let `before(E1) = before(N)`
+/// - Let `before(E2) = after(E1)`
+/// - Let `T` be the static return type of the invocation
+/// - If `T <: Never` then:
+///   - Let `after(N) = unreachable(after(E2))`.
+/// - Otherwise:
+///   - Let `after(N) = after(E2)`.
+///
+/// @description Checks that for an expression of the form `E1.m1(E2)`
+/// `before(E2) = after(E1)`. Test that if `after(E1)` is unreachable then
+/// `before(E2)` is also unreachable.
+/// @author [email protected]
+
+void test<T extends Never>(T n) {
+  late int i;
+  if (2 > 1) {
+    n.foo(i = 42);
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test);
+}

TypeSystem/flow-analysis/reachability_A22_t02.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 - Method invocation: If `N` is an expression of the form
+/// `E1.m1(E2)`, then:
+/// - Let `before(E1) = before(N)`
+/// - Let `before(E2) = after(E1)`
+/// - Let `T` be the static return type of the invocation
+/// - If `T <: Never` then:
+///   - Let `after(N) = unreachable(after(E2))`.
+/// - Otherwise:
+///   - Let `after(N) = after(E2)`.
+///
+/// @description Checks that for an expression of the form `E1.m1(E2)`
+/// `before(E2) = after(E1)`. Test that if `after(E1)` is unreachable then
+/// `before(E2)` is also unreachable.
+/// @author [email protected]
+
+class C {
+  C(int i);
+  void foo(int j) {}
+}
+
+void test<T extends Never>(T n) {
+  late int i;
+  if (2 > 1) {
+    C(n).foo(i = 42);
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test);
+}

TypeSystem/flow-analysis/reachability_A22_t03.dart

@@ -0,0 +1,63 @@
+// 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 - Method invocation: If `N` is an expression of the form
+/// `E1.m1(E2)`, then:
+/// - Let `before(E1) = before(N)`
+/// - Let `before(E2) = after(E1)`
+/// - Let `T` be the static return type of the invocation
+/// - If `T <: Never` then:
+///   - Let `after(N) = unreachable(after(E2))`.
+/// - Otherwise:
+///   - Let `after(N) = after(E2)`.
+///
+/// @description Checks that if the static type of the expression of the form
+/// `E1.m1(E2)` is `Never` `after(N) = unreachable(after(E2))`.
+/// @author [email protected]
+
+class C<T extends Never> {
+  T foo() => throw "";
+  Future<T> bar() async {
+    throw "";
+  }
+}
+
+void test1() {
+  late int i;
+  if (2 > 1) {
+    C().foo();
+    i = 42;
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+void test2() {
+  late int i;
+  if (2 > 1) {
+    C().bar(); // Return type is not `Never`
+    i = 42;
+  }
+  i; // Not definitely unassigned
+}
+
+void test3() async {
+  late int i;
+  if (2 > 1) {
+    await C().bar();
+    i = 42;
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test1);
+  print(test2);
+  print(test3);
+}

TypeSystem/flow-analysis/reachability_A22_t04.dart

@@ -0,0 +1,63 @@
+// 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 - Method invocation: If `N` is an expression of the form
+/// `E1.m1(E2)`, then:
+/// - Let `before(E1) = before(N)`
+/// - Let `before(E2) = after(E1)`
+/// - Let `T` be the static return type of the invocation
+/// - If `T <: Never` then:
+///   - Let `after(N) = unreachable(after(E2))`.
+/// - Otherwise:
+///   - Let `after(N) = after(E2)`.
+///
+/// @description Checks that if the static type of the expression of the form
+/// `E1.m1(E2)` is `Never` then `E2` is still reachable.
+/// @author [email protected]
+
+class C<T extends Never> {
+  T foo(int x) => throw "foo";
+  T bar([int x = 0]) => throw "bar";
+  T baz({int x = 0}) => throw "baz";
+  T qux({required int x}) => throw "qux";
+}
+
+void test1() {
+  late int i;
+  try {
+    C().foo(i = 42);
+  } catch (_) {}
+  i; // Not definitely unassigned
+}
+
+void test2() {
+  late int i;
+  try {
+    C().bar(i = 42);
+  } catch (_) {}
+  i;
+}
+
+void test3() {
+  late int i;
+  try {
+    C().baz(x: i = 42);
+  } catch (_) {}
+  i;
+}
+
+void test4() {
+  late int i;
+  try {
+    C().qux(x: i = 42);
+  } catch (_) {}
+  i;
+}
+
+main() {
+  test1();
+  test2();
+  test3();
+  test4();
+}

TypeSystem/flow-analysis/reachability_A22_t05.dart

@@ -0,0 +1,57 @@
+// 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 - Method invocation: If `N` is an expression of the form
+/// `E1.m1(E2)`, then:
+/// - Let `before(E1) = before(N)`
+/// - Let `before(E2) = after(E1)`
+/// - Let `T` be the static return type of the invocation
+/// - If `T <: Never` then:
+///   - Let `after(N) = unreachable(after(E2))`.
+/// - Otherwise:
+///   - Let `after(N) = after(E2)`.
+///
+/// @description Checks that for an expression of the form `E1.m1(E2)`, if the
+/// static type of `E1` is not `Never` then `after(N) = after(E2)`. This is
+/// tested by detecting that `i = 42` is considered to be guaranteed to have
+/// been executed when `i;` is executed.
+/// @author [email protected]
+
+class C {
+  void foo(int x) {}
+  void bar([int x = 0]) {}
+  void baz({int x = 0}) {}
+  void qux({required int x}) {}
+}
+
+void test1() {
+  int i;
+  C().foo(i = 42);
+  i; // Definitely assigned
+}
+
+void test2() {
+  int i;
+  C().bar(i = 42);
+  i; // Definitely assigned
+}
+
+void test3() {
+  int i;
+  C().baz(x: i = 42);
+  i; // Definitely assigned
+}
+
+void test4() {
+  int i;
+  C().qux(x: i = 42);
+  i; // Definitely assigned
+}
+
+main() {
+  test1();
+  test2();
+  test3();
+  test4();
+}

TypeSystem/flow-analysis/reachability_A22_t06.dart

@@ -0,0 +1,58 @@
+// 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 - Method invocation: If `N` is an expression of the form
+/// `E1.m1(E2)`, then:
+/// - Let `before(E1) = before(N)`
+/// - Let `before(E2) = after(E1)`
+/// - Let `T` be the static return type of the invocation
+/// - If `T <: Never` then:
+///   - Let `after(N) = unreachable(after(E2))`.
+/// - Otherwise:
+///   - Let `after(N) = after(E2)`.
+///
+/// @description Checks that for an expression of the form `E1.m1(E2)`, if the
+/// static type of `E1` is not `Never` then `after(N) = after(E2)`. This is
+/// tested by detecting that `i = 42` is considered to be guaranteed to have
+/// been executed when `i;` is executed. Test the case when `m1` is a getter
+/// returning a function type.
+/// @author [email protected]
+
+class C {
+  void Function(int) get foo => (int x) {};
+  void Function([int]) get bar => ([int x = 0]) {};
+  void Function({int x}) get baz => ({int x = 0}) {};
+  void Function({required int x}) get qux => ({required int x}) {};
+}
+
+void test1() {
+  int i;
+  C().foo(i = 42);
+  i; // Definitely assigned
+}
+
+void test2() {
+  int i;
+  C().bar(i = 42);
+  i; // Definitely assigned
+}
+
+void test3() {
+  int i;
+  C().baz(x: i = 42);
+  i; // Definitely assigned
+}
+
+void test4() {
+  int i;
+  C().qux(x: i = 42);
+  i; // Definitely assigned
+}
+
+main() {
+  test1();
+  test2();
+  test3();
+  test4();
+}

TypeSystem/flow-analysis/reachability_A22_t07.dart

@@ -0,0 +1,50 @@
+// 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 - Method invocation: If `N` is an expression of the form
+/// `E1.m1(E2)`, then:
+/// - Let `before(E1) = before(N)`
+/// - Let `before(E2) = after(E1)`
+/// - Let `T` be the static return type of the invocation
+/// - If `T <: Never` then:
+///   - Let `after(N) = unreachable(after(E2))`.
+/// - Otherwise:
+///   - Let `after(N) = after(E2)`.
+///
+/// @description Checks that for an expression of the form `E1.m1(E2)`
+/// `before(E2) = after(E1)`. Test that if `m1` is a getter returning type
+/// `Never` then `before(E2)` is unreachable.
+/// @author [email protected]
+
+class C<T extends Never> {
+  Never get foo => throw "Never";
+  T get bar => throw "Never";
+}
+
+void test1() {
+  late int i;
+  if (2 > 1) {
+    C().foo(i = 42); // ignore: receiver_of_type_never
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+void test2() {
+  late int i;
+  if (2 > 1) {
+    C().bar(i = 42);  // ignore: receiver_of_type_never
+  }
+  i; // Definitely unassigned
+//^
+// [analyzer] unspecified
+// [cfe] unspecified
+}
+
+main() {
+  print(test1);
+  print(test2);
+}