Skip to content

Fixes #3143. Update assertions, add language version, add new tests #3144

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Apr 15, 2025
Merged

Fixes #3143. Update assertions, add language version, add new tests #3144

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cb32f77
Fixes #3143. Update assertions, add language version, add new tests
sgrekhov Apr 14, 2025
8ad57dd
Apply review suggestions.
sgrekhov Apr 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 10 additions & 18 deletions TypeSystem/flow-analysis/reachability_A07_t01.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,17 @@
// 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 If N is an expression of the form E1.m1(E2), then:
/// @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)`
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
///
/// @description Checks reachability after method call. Test return type Never
/// @description Checks reachability after method call. Test return type `Never`
/// @author sgrekhov@unipro.ru

class C {
Expand Down
28 changes: 10 additions & 18 deletions TypeSystem/flow-analysis/reachability_A07_t02.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,26 +2,18 @@
// 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 If N is an expression of the form E1.m1(E2), then:
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
/// @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 reachability after method call. Test static method and
/// return type Never
/// return type `Never`
/// @author sgrekhov@unipro.ru

class C {
Expand Down
29 changes: 11 additions & 18 deletions TypeSystem/flow-analysis/reachability_A07_t03.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,18 @@
// 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 If N is an expression of the form E1.m1(E2), then:
/// @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)`
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
///
/// @description Checks reachability after method call. Test return type T <: Null
/// @description Checks reachability after method call. Test return type
/// `T <: Null`
/// @author sgrekhov@unipro.ru
/// @issue 41981

Expand Down
28 changes: 10 additions & 18 deletions TypeSystem/flow-analysis/reachability_A07_t04.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,26 +2,18 @@
// 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 If N is an expression of the form E1.m1(E2), then:
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
/// @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 reachability after method call. Test static method with
/// the return type T <: Null
/// the return type `T <: Null`
/// @author sgrekhov@unipro.ru
/// @issue 41981

Expand Down
29 changes: 11 additions & 18 deletions TypeSystem/flow-analysis/reachability_A07_t05.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,18 @@
// 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 If N is an expression of the form E1.m1(E2), then:
/// @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)`
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
///
/// @description Checks reachability after method call. Test return type T <: Null
/// @description Checks reachability after method call. Test return type
/// `T <: Null`
/// @author sgrekhov@unipro.ru
/// @issue 41985

Expand Down
28 changes: 10 additions & 18 deletions TypeSystem/flow-analysis/reachability_A07_t06.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,26 +2,18 @@
// 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 If N is an expression of the form E1.m1(E2), then:
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
/// @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 reachability after method call. Test static method and
/// return type T <: Null
/// return type `T <: Null`
/// @author sgrekhov@unipro.ru
/// @issue 41985

Expand Down
34 changes: 14 additions & 20 deletions TypeSystem/flow-analysis/reachability_A07_t07.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,29 +2,23 @@
// 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 If N is an expression of the form E1.m1(E2), then:
/// @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)`
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
///
/// @description Checks reachability after method call. Test non-nullable return
/// type
/// @description Checks reachability after method invocation. Tests a method
/// with a non-nullable return type.
/// @author sgrekhov@unipro.ru
/// @issue 41985

// @dart = 3.8

import "../../Utils/expect.dart";

class C {
Expand All @@ -36,7 +30,7 @@ main() {
late int i;
if (c.m1() == null) {
i = 42; // `i` is not definitely unassigned because in a weak mode the
// condition may be true
// condition may be `true` (Dart 3.8 and earlier)
}
try {
i;
Expand Down
34 changes: 14 additions & 20 deletions TypeSystem/flow-analysis/reachability_A07_t08.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,29 +2,23 @@
// 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 If N is an expression of the form E1.m1(E2), then:
/// @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)`
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
///
/// @description Checks reachability after method call. Test static method and
/// non-nullable return type
/// @description Checks reachability after method invocation. Tests a static
/// method with a non-nullable return type.
/// @author sgrekhov@unipro.ru
/// @issue 41985

// @dart = 3.8

import "../../Utils/expect.dart";

class C {
Expand All @@ -35,7 +29,7 @@ main() {
late int i;
if (C.m1() == null) {
i = 42; // `i` is not definitely unassigned because in a weak mode the
// condition may be true
// condition may be `true` (Dart 3.8 and earlier)
}
try {
i;
Expand Down
34 changes: 14 additions & 20 deletions TypeSystem/flow-analysis/reachability_A07_t09.dart
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,29 +2,23 @@
// 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 If N is an expression of the form E1.m1(E2), then:
/// @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)`
///
/// Let before(E1) = before(N)
/// Let before(E2) = after(E2)
/// Let T be the static return type of the invocation
/// 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) = before(N).
/// Let notNull(N) = unreachable(before(N)).
/// Otherwise:
/// Let null(N) = promote(x, Null, before(N))
/// Let notNull(N) = promoteToNonNull(x, before(N))
///
/// @description Checks reachability after method call. Test non-nullable return
/// type
/// @description Checks reachability after method invocation. Tests a method
/// with a non-nullable return type.
/// @author sgrekhov@unipro.ru
/// @issue 41985

// @dart = 3.8

class C {
String m1() => "Lily was here";
}
Expand All @@ -34,7 +28,7 @@ main() {
int i;
if (c.m1() != null) {
i = 42; // `i` is not definitely assigned because in a weak mode the
// condition may be false
// condition may be `false` (Dart 3.8 and earlier)
}
i; // It is an error to read a local non-nullable variable which is not definitely assigned
//^
Expand Down
Loading