diff --git a/TypeSystem/flow-analysis/reachability_A08_t01.dart b/TypeSystem/flow-analysis/reachability_A08_t01.dart index 0cf6148a0d..a57ad5d598 100644 --- a/TypeSystem/flow-analysis/reachability_A08_t01.dart +++ b/TypeSystem/flow-analysis/reachability_A08_t01.dart @@ -2,21 +2,34 @@ // 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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). /// -/// 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 Null +/// @description Checks that if `equivalentToNull(T1)` and +/// `equivalentToNull(T2)`, then `true(N) = after(E2)` and +/// `false(N) = unreachable(after(E2))`. /// @author sgrekhov@unipro.ru /// @issue 41985 @@ -24,9 +37,17 @@ main() { int i; - Null n = null; - if (n == null) { + late int j; + Null n1 = null; + Null n2 = null; + if (n1 == n2) { i = 42; // condition is always true therefore `i` must be definitely assigned + } else { + j = 42; } i; // It's not an error to read local non-nullable variable if it is definitely assigned + j; // Still definitely unassigned +//^ +// [analyzer] unspecified +// [cfe] unspecified } diff --git a/TypeSystem/flow-analysis/reachability_A08_t02.dart b/TypeSystem/flow-analysis/reachability_A08_t02.dart index b5288dacef..b3d4629be0 100644 --- a/TypeSystem/flow-analysis/reachability_A08_t02.dart +++ b/TypeSystem/flow-analysis/reachability_A08_t02.dart @@ -2,32 +2,53 @@ // 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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). /// -/// 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 Null +/// @description Checks that if `equivalentToNull(T1)` and +/// `equivalentToNull(T2)`, then `true(N) = after(E2)` and +/// `false(N) = unreachable(after(E2))`. Test getter of type `Null`. /// @author sgrekhov@unipro.ru /// @issue 41985 // Requirements=nnbd-strong -Null get n => null; +Null get n1 => null; main() { int i; - if (n == null) { + late int j; + Null n2; + if (n1 == n2) { i = 42; // condition is always true therefore `i` must be definitely assigned + } else { + j = 42; } i; // It's not an error to read local non-nullable variable if it is definitely assigned + j; // Still definitely unassigned +//^ +// [analyzer] unspecified +// [cfe] unspecified } diff --git a/TypeSystem/flow-analysis/reachability_A08_t03.dart b/TypeSystem/flow-analysis/reachability_A08_t03.dart new file mode 100644 index 0000000000..cf3beb5f71 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A08_t03.dart @@ -0,0 +1,73 @@ +// 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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). +/// +/// @description Checks that if `equivalentToNull(T1)` and `T2` is non-nullable, +/// or `equivalentToNull(T2)` and `T1` is non-nullable then +/// `true(N) = unreachable(after(E2))` and `false(N) = after(E2)`. +/// @author sgrekhov22@gmail.com +/// @issue 60114 + +// Requirements=nnbd-strong + +test1(T t) { + late int i; + int j; + String s = ""; + if (s == t) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely unassigned + } else { + j = 42; + } + i; +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; // Definitely assigned +} + +test2(T t) { + late int i; + int j; + String s = ""; + if (t == s) { // ignore: unnecessary_null_comparison + i = 42; + } else { + j = 42; + } + i; +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; +} + +main() { + print(test1); + print(test2); +} diff --git a/TypeSystem/flow-analysis/reachability_A08_t04.dart b/TypeSystem/flow-analysis/reachability_A08_t04.dart index 0a077c5a42..3426f88860 100644 --- a/TypeSystem/flow-analysis/reachability_A08_t04.dart +++ b/TypeSystem/flow-analysis/reachability_A08_t04.dart @@ -2,39 +2,51 @@ // 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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). /// -/// 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 non-nullable -/// type +/// @description Checks that if `equivalentToNull(T2)` and `T1` is non-nullable, +/// then `true(N) = unreachable(after(E2))` and `false(N) = after(E2)`. /// @author sgrekhov@unipro.ru /// @issue 41981 +/// @issue 60114 // Requirements=nnbd-strong -import "../../Utils/expect.dart"; - main() { late int i; + int j; String s = ""; - if (s == null) { - i = 42; // `i` is not definitely unassigned because in a weak mode the - // condition may be true - } - try { - i; - Expect.fail("Error expected"); - } on Error catch(e) { - // Ok + if (s == null) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely unassigned + } else { + j = 42; } + i; +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; } diff --git a/TypeSystem/flow-analysis/reachability_A08_t05.dart b/TypeSystem/flow-analysis/reachability_A08_t05.dart index ba0e271fae..1fae566cee 100644 --- a/TypeSystem/flow-analysis/reachability_A08_t05.dart +++ b/TypeSystem/flow-analysis/reachability_A08_t05.dart @@ -2,40 +2,52 @@ // 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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). /// -/// 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 -/// non-nullable type +/// @description Checks that if `equivalentToNull(T1)` and `T2` is non-nullable, +/// then `true(N) = unreachable(after(E2))` and `false(N) = after(E2)`. /// @author sgrekhov@unipro.ru /// @issue 41981 +/// @issue 60114 // Requirements=nnbd-strong -import "../../Utils/expect.dart"; - String get s => "Lily was here"; main() { late int i; - if (s == null) { - i = 42; // `i` is not definitely unassigned because in a weak mode the - // condition may be true - } - try { - i; - Expect.fail("Error expected"); - } on Error catch(e) { - // Ok + int j; + if (null == s) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely unassigned + } else { + j = 42; } + i; +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; // Definitely assigned } diff --git a/TypeSystem/flow-analysis/reachability_A08_t06.dart b/TypeSystem/flow-analysis/reachability_A08_t06.dart new file mode 100644 index 0000000000..cf3beb5f71 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A08_t06.dart @@ -0,0 +1,73 @@ +// 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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). +/// +/// @description Checks that if `equivalentToNull(T1)` and `T2` is non-nullable, +/// or `equivalentToNull(T2)` and `T1` is non-nullable then +/// `true(N) = unreachable(after(E2))` and `false(N) = after(E2)`. +/// @author sgrekhov22@gmail.com +/// @issue 60114 + +// Requirements=nnbd-strong + +test1(T t) { + late int i; + int j; + String s = ""; + if (s == t) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely unassigned + } else { + j = 42; + } + i; +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; // Definitely assigned +} + +test2(T t) { + late int i; + int j; + String s = ""; + if (t == s) { // ignore: unnecessary_null_comparison + i = 42; + } else { + j = 42; + } + i; +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; +} + +main() { + print(test1); + print(test2); +} diff --git a/TypeSystem/flow-analysis/reachability_A08_t07.dart b/TypeSystem/flow-analysis/reachability_A08_t07.dart new file mode 100644 index 0000000000..23834b7627 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A08_t07.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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). +/// +/// @description Checks that if `stripParens(E1)` is a `null` literal, then +/// `true(N) = after(E2)` and `false(N) = promoteToNonNull(E2, after(E2))`. +/// @author sgrekhov22@gmail.com + +test(int? n) { + if ((null) == n) { + n.isEven; +// ^ +// [analyzer] unspecified +// [cfe] unspecified + } else { + n.isEven; + } +} + +main() { + print(test); +} diff --git a/TypeSystem/flow-analysis/reachability_A08_t08.dart b/TypeSystem/flow-analysis/reachability_A08_t08.dart new file mode 100644 index 0000000000..c945d08a87 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A08_t08.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 operator== If `N` is an expression of the form `E1 == E2`, where +/// the static type of `E1` is `T1` and the static type of `E2` is `T2`, then: +/// - Let `before(E1) = before(N)`. +/// - Let `before(E2) = after(E1)`. +/// - If `equivalentToNull(T1)` and `equivalentToNull(T2)`, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = unreachable(after(E2))`. +/// - Otherwise, if `equivalentToNull(T1)` and `T2` is non-nullable, or +/// `equivalentToNull(T2)` and `T1` is non-nullable, then: +/// - Let `true(N) = unreachable(after(E2))`. +/// - Let `false(N) = after(E2)`. +/// - Otherwise, if `stripParens(E1)` is a `null` literal, then: +/// - Let `true(N) = after(E2)`. +/// - Let `false(N) = promoteToNonNull(E2, after(E2))`. +/// - Otherwise, if `stripParens(E2)` is a `null` literal, then: +/// - Let `true(N) = after(E1)`. +/// - Let `false(N) = promoteToNonNull(E1, after(E2))`. +/// - Otherwise: +/// - Let after(N) = after(E2). +/// Note that it is tempting to generalize the two `null` literal cases to apply +/// to any expression whose type is `Null`, but this would be unsound in cases +/// where `E2` assigns to `x`. (Consider, for example, +/// `(int? x) => x == (x = null) ? true : x.isEven`, which tries to call +/// `null.isEven` in the event of a non-null input). +/// +/// @description Checks that if `stripParens(E2)` is a `null` literal, then +/// `true(N) = after(E1)` and `false(N) = promoteToNonNull(E1, after(E2))`. +/// @author sgrekhov22@gmail.com + +test(int? n) { + if (n == (null)) { + n.isEven; +// ^ +// [analyzer] unspecified +// [cfe] unspecified + } else { + n.isEven; + } +} + +main() { + print(test); +} diff --git a/TypeSystem/flow-analysis/reachability_A09_t01.dart b/TypeSystem/flow-analysis/reachability_A09_t01.dart index 0c18dc74e2..96417717ef 100644 --- a/TypeSystem/flow-analysis/reachability_A09_t01.dart +++ b/TypeSystem/flow-analysis/reachability_A09_t01.dart @@ -2,32 +2,28 @@ // 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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. /// -/// 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 Null +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `equivalentToNull(T1)` and +/// `equivalentToNull(T2) case. /// @author sgrekhov@unipro.ru /// @issue 41981 main() { late int i; - Null n = null; - if (n != null) { + int j; + Null n1 = null; + Null n2 = null; + if (n1 != n2) { i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned + } else { + j = 42; } i; // It is an error to read a local late variable when it is definitely unassigned. //^ // [analyzer] unspecified // [cfe] unspecified + j; // Definitely assigned } diff --git a/TypeSystem/flow-analysis/reachability_A09_t02.dart b/TypeSystem/flow-analysis/reachability_A09_t02.dart index 01669f9b57..98dda050a3 100644 --- a/TypeSystem/flow-analysis/reachability_A09_t02.dart +++ b/TypeSystem/flow-analysis/reachability_A09_t02.dart @@ -2,33 +2,29 @@ // 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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. /// -/// 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 Null +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `equivalentToNull(T1)` and +/// `equivalentToNull(T2) case and getter of the type `Null`. /// @author sgrekhov@unipro.ru /// @issue 41981 -Null get n => null; +Null get n1 => null; main() { late int i; - if (n != null) { + int j; + Null n2; + if (n1 != n2) { i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned + } else { + j = 42; } i; // It is an error to read a local late variable when it is definitely unassigned. //^ // [analyzer] unspecified // [cfe] unspecified + j; // Definitely assigned } diff --git a/TypeSystem/flow-analysis/reachability_A09_t03.dart b/TypeSystem/flow-analysis/reachability_A09_t03.dart new file mode 100644 index 0000000000..de337d026e --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A09_t03.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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. +/// +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `equivalentToNull(T1)` and +/// `equivalentToNull(T2) case. +/// @author sgrekhov22@gmail.com + +test1(T t) { + late int i; + int j; + Null n = null; + if (n != t) { + i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned + } else { + j = 42; + } + i; // It is an error to read a local late variable when it is definitely unassigned. +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; // Definitely assigned +} + +test2(T t) { + late int i; + int j; + Null n = null; + if (t != n) { + i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned + } else { + j = 42; + } + i; // It is an error to read a local late variable when it is definitely unassigned. +//^ +// [analyzer] unspecified +// [cfe] unspecified + j; +} + +main() { + print(test1); + print(test2); +} diff --git a/TypeSystem/flow-analysis/reachability_A09_t04.dart b/TypeSystem/flow-analysis/reachability_A09_t04.dart index 796a486c11..80fa5647e0 100644 --- a/TypeSystem/flow-analysis/reachability_A09_t04.dart +++ b/TypeSystem/flow-analysis/reachability_A09_t04.dart @@ -2,32 +2,27 @@ // 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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. /// -/// 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 non-nullable -/// type +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `equivalentToNull(T2)` and +/// `T1` is non-nullable case. /// @author sgrekhov@unipro.ru /// @issue 41985 +/// @issue 60114 main() { int i; + late int j; String s = ""; - if (s != null) { - i = 42; // `i` is not definitely assigned because in a weak mode the - // condition may be false + if (s != null) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely assigned here + } else { + j = 42; } - i; // It is an error to read a local non-nullable variable which is not definitely assigned + i; // It is not an error to read a local non-nullable variable which is definitely assigned + j; // Still definitely unassigned //^ // [analyzer] unspecified // [cfe] unspecified diff --git a/TypeSystem/flow-analysis/reachability_A09_t05.dart b/TypeSystem/flow-analysis/reachability_A09_t05.dart index 2d42345590..a3e0e984c7 100644 --- a/TypeSystem/flow-analysis/reachability_A09_t05.dart +++ b/TypeSystem/flow-analysis/reachability_A09_t05.dart @@ -2,33 +2,29 @@ // 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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. /// -/// 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 -/// non-nullable type +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `equivalentToNull(T1)` and +/// `T2` is non-nullable, or `equivalentToNull(T2)` and `T1` is non-nullable +/// case. /// @author sgrekhov@unipro.ru /// @issue 41985 +/// @issue 60114 String get s => "Lily was here"; main() { int i; - if (s != null) { - i = 42; // `i` is not definitely assigned because in a weak mode the - // condition may be false + late int j; + if (null != s) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely assigned here + } else { + j = 42; } - i; // It is an error to read a local non-nullable variable which is not definitely assigned + i; // It is not an error to read a local non-nullable variable which is definitely assigned + j; // Still definitely unassigned //^ // [analyzer] unspecified // [cfe] unspecified diff --git a/TypeSystem/flow-analysis/reachability_A09_t06.dart b/TypeSystem/flow-analysis/reachability_A09_t06.dart new file mode 100644 index 0000000000..b9ae3fbe1e --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A09_t06.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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. +/// +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `equivalentToNull(T1)` and +/// `T2` is non-nullable, or `equivalentToNull(T2)` and `T1` is non-nullable +/// case. +/// @author sgrekhov22@gmail.com +/// @issue 60114 + +test1(T t) { + int i; + late int j; + String s = ""; + if (s != t) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely assigned here + } else { + j = 42; + } + i; // It is not an error to read a local non-nullable variable which is definitely assigned + j; // Still definitely unassigned +//^ +// [analyzer] unspecified +// [cfe] unspecified +} + +test2(T t) { + int i; + late int j; + String s = ""; + if (t != s) { // ignore: unnecessary_null_comparison + i = 42; // `i` is definitely assigned here + } else { + j = 42; + } + i; // It is not an error to read a local non-nullable variable which is definitely assigned + j; // Still definitely unassigned +//^ +// [analyzer] unspecified +// [cfe] unspecified +} + +main() { + test1(null); + test2(null); +} diff --git a/TypeSystem/flow-analysis/reachability_A09_t07.dart b/TypeSystem/flow-analysis/reachability_A09_t07.dart new file mode 100644 index 0000000000..5b0a12b801 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A09_t07.dart @@ -0,0 +1,26 @@ +// 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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. +/// +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `stripParens(E1)` is a +/// `null` literal case. +/// @author sgrekhov22@gmail.com + +test(int? n) { + if ((null) != n) { + n.isEven; + } else { + n.isEven; +// ^^^^^^ +// [analyzer] unspecified +// [cfe] unspecified + } +} + +main() { + print(test); +} diff --git a/TypeSystem/flow-analysis/reachability_A09_t08.dart b/TypeSystem/flow-analysis/reachability_A09_t08.dart new file mode 100644 index 0000000000..551bd79ec5 --- /dev/null +++ b/TypeSystem/flow-analysis/reachability_A09_t08.dart @@ -0,0 +1,26 @@ +// 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 operator!= If `N` is an expression of the form `E1 != E2`, it is +/// treated as equivalent to the expression `!(E1 == E2)`. +/// +/// @description Checks that an expression of the form `E1 != E2` is treated as +/// equivalent to the expression `!(E1 == E2)`. Test `stripParens(E2)` is a +/// `null` literal case. +/// @author sgrekhov22@gmail.com + +test(int? n) { + if (n != (null)) { + n.isEven; + } else { + n.isEven; +// ^^^^^^ +// [analyzer] unspecified +// [cfe] unspecified + } +} + +main() { + print(test); +}