Positive coverage: prove_eq / existential
existential| Line | Coverage | Source |
|---|---|---|
| 62 | 5 | (prove_existential_var_eq(decls, env, assumptions, v, r) => c) |
| ──────── ("existential") | ||
| 64 | 141 | (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c) |
141 tests exercised this rule:
Source location: crates/formality-rust/src/prove/test/eq_assumptions.rs:24 (all coverage from this test)
#[test]
fn test_b() {
test_prove(
Program::empty(),
term("exists<A> {} => {for<T, U> if {T = u32, U = Vec<T>} A = U}"),
)
.assert_ok(expect!["{Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => Vec<u32>, ?ty_2 => u32} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (forall)prove_wc.rs:36args
prove_wc (implies)prove_wc.rs:42args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (normalize-l)prove_eq.rs:70args
prove_normalize (normalize-via-assumption)prove_normalize.rs:33args
prove_normalize_via (axiom-l)prove_normalize.rs:97args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (normalize-l)prove_eq.rs:70args
prove_normalize (normalize-via-assumption)prove_normalize.rs:33args
prove_normalize_via (axiom-l)prove_normalize.rs:97args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: crates/formality-rust/src/prove/test/eq_partial_eq.rs:25 (all coverage from this test)
#[test]
fn eq_implies_partial_eq() {
let assumptions: Wcs = Wcs::t();
let goal: Wc = term("for<T> if {Eq(T)} PartialEq(T)");
let constraints = prove(decls(), (), assumptions, goal);
constraints.assert_ok(
expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (forall)prove_wc.rs:36args
prove_wc (implies)prove_wc.rs:42args
prove_wc (trait implied bound)prove_wc.rs:114args
prove_via (predicate-congruence-axiom)prove_via.rs:32args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (assumption)prove_wc.rs:49args
prove_via (predicate-congruence-axiom)prove_via.rs:32args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: crates/formality-rust/src/prove/test/exists_constraints.rs:24 (all coverage from this test)
#[test]
fn exists_u_for_t() {
test_prove(decls(), term("exists<U> {} => {Foo(U)}")).assert_ok(expect!["{Constraints { env: Env { variables: [?ty_2, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => Vec<?ty_2>} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: crates/formality-rust/src/prove/test/occurs_check.rs:36 (all coverage from this test)
#[test]
fn eq_variable_to_rigid() {
test_prove(decls(), term("exists<X, Y> {} => {X = Vec<Y>}")).assert_ok(expect!["{Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => Vec<?ty_3>, ?ty_2 => ?ty_3} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: crates/formality-rust/src/prove/test/occurs_check.rs:42 (all coverage from this test)
#[test]
fn eq_rigid_to_variable() {
test_prove(decls(), term("exists<X, Y> {} => {Vec<Y> = X}")).assert_ok(expect!["{Constraints { env: Env { variables: [?ty_3, ?ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => Vec<?ty_3>, ?ty_2 => ?ty_3} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: crates/formality-rust/src/prove/test/simple_impl.rs:24 (all coverage from this test)
#[test]
fn vec_u32_debug() {
let goal: Wc = term("Debug(Vec<u32>)");
prove(decls(), (), (), goal).assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (rigid)prove_eq.rs:48args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: crates/formality-rust/src/prove/test/simple_impl.rs:30 (all coverage from this test)
#[test]
fn vec_vec_u32_debug() {
let goal: Wc = term("Debug(Vec<Vec<u32>>)");
prove(decls(), (), (), goal).assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (rigid)prove_eq.rs:48args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (rigid)prove_eq.rs:48args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: crates/formality-rust/src/prove/test/universes.rs:37 (all coverage from this test)
#[test]
fn for_t_exists_u() {
let decls = Program {
crates: Arc::new(Program::program_from_items(vec![
term("trait Test<T> where {}"),
term("impl<X> Test<X> for X {}"),
])),
..Program::empty()
};
test_prove(decls, term("{} => {for<T> Test(T, T)}")).assert_ok(expect!["{Constraints { env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (forall)prove_wc.rs:36args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-universal)prove_eq.rs:141args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: tests/associated_type_normalization.rs:19 (all coverage from this test)
#[test]
fn test_mirror_normalizes_u32_to_u32() {
test_where_clause(MIRROR, "exists<T> {} => {<u32 as Mirror>::Assoc = T}")
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => <u32 as Mirror>::Assoc} }}"]);
}
Proof tree
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (normalize-l)prove_eq.rs:70args
prove_normalize (normalize-via-impl)prove_normalize.rs:48args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_eq (symmetric)prove_eq.rs:39args
prove_eq (existential)prove_eq.rs:63args
prove_existential_var_eq (existential-nonvar)prove_eq.rs:96args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
Source location: tests/basic_tests.rs:58 (all coverage from this test)
#[test]
fn hello_world() {
FormalityTest::new(crates![crate Foo {
trait Foo<T> where T: Bar<Self>, Self: Baz {}
trait Bar<T> where T: Baz {}
trait Baz {}
impl Baz for u32 {}
impl Bar<u32> for u32 {}
impl<T> Bar<T> for () where T: Baz {}
}])
.skip_execute()
.ok()
}
Proof tree
check_all_crates (check all prefixes)mod.rs:54args
for_allmod.rs:41for_allmod.rs:51args
check_crate (check crate)mod.rs:75args
for_allmod.rs:60for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (none)prove_wc_list.rs:21args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
for_allmod.rs:72args
check_crate_item (trait impl)mod.rs:195args
check_trait_impl (check_trait_impl)impls.rs:41args
prove_wc_list (none)prove_wc_list.rs:21args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (positive impl)prove_wc.rs:81args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (eq)prove_wc.rs:120args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
Source location: tests/basic_tests.rs:74 (all coverage from this test)
#[test]
fn basic_where_clauses_pass() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
trait WellFormed where for<T> u32: A<T> { }
impl <T> B for T {}
}])
.skip_execute()
.ok()
}
Proof trees omitted for the remaining 131 tests; each one is on its test’s page in Coverage by test.
Source location: tests/basic_tests.rs:121 (all coverage from this test)
fn foo() -> () where for<T> u32: A<T> { trusted }
impl <T> B for T {}
}])
p_execute()
)
}
#[test]
ifetime_binder_in_fn_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }
trait B { }
fn foo() -> () where for<T> u32: A<T> { trusted }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
#[test]
ifetime_binder_in_trait_impl_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
impl<T> B for T where for<U> u32: A<U> { }
}])
p_execute()
)
}
#[test]
ifetime_binder_in_trait_impl_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }
trait B { }
impl<T> B for T where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
#[test]
ifetime_binder_in_neg_trait_impl_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
impl<T> !A<T> for u32 where for<U> u32: A<U> { }
impl <T> B for T {}
}])
p_execute()
)
}
#[test]
ifetime_binder_in_neg_trait_impl_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }
trait B { }
impl<T> !A<T> for u32 where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
#[test]
ifetime_binder_in_enum_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
enum E where for<U> u32: A<U> { }
impl <T> B for T {}
}])
p_execute()
)
}
#[test]
ifetime_binder_in_enum_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }
trait B { }
enum E where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
#[test]
ifetime_binder_in_struct_where_clause_pass() {
alityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
struct S<T> where for<U> u32: A<U> { }
impl <T> B for T {}
}])
p_execute()
)
}
#[test]
ifetime_binder_in_struct_where_clause_fail() {
alityTest::new(crates![crate core {
trait A<T> where T: B { }
trait B { }
struct S<T> where for<U> u32: A<U> { }
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
non lifetime binders require #![feature(non_lifetime_binders)]"#]])
}
#[test]
ime_binder_in_where_clause_without_feature_pass() {
alityTest::new(crates![crate core {
trait A<'b> { }
impl<'b> A<'b> for u32 { }
trait WellFormed where for<'b> u32: A<'b> { }
}])
p_execute()
)
}
#[test]
_adt_variant_dup() {
alityTest::new(crates![crate Foo {
enum Bar {
Baz{},
Baz{},
}
Source location: tests/basic_tests.rs:149 (all coverage from this test)
#[test]
fn non_lifetime_binder_in_trait_impl_where_clause_pass() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
impl<T> B for T where for<U> u32: A<U> { }
}])
.skip_execute()
.ok()
}
Source location: tests/basic_tests.rs:179 (all coverage from this test)
#[test]
fn non_lifetime_binder_in_neg_trait_impl_where_clause_pass() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
impl<T> !A<T> for u32 where for<U> u32: A<U> { }
impl <T> B for T {}
}])
.skip_execute()
.ok()
}
Source location: tests/basic_tests.rs:209 (all coverage from this test)
#[test]
fn non_lifetime_binder_in_enum_where_clause_pass() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
enum E where for<U> u32: A<U> { }
impl <T> B for T {}
}])
.skip_execute()
.ok()
}
Source location: tests/basic_tests.rs:239 (all coverage from this test)
#[test]
fn non_lifetime_binder_in_struct_where_clause_pass() {
FormalityTest::new(crates![crate core {
#![feature(non_lifetime_binders)]
trait A<T> where T: B { }
trait B { }
struct S<T> where for<U> u32: A<U> { }
impl <T> B for T {}
}])
.skip_execute()
.ok()
}
Source location: tests/basic_tests.rs:266 (all coverage from this test)
#[test]
fn lifetime_binder_in_where_clause_without_feature_pass() {
FormalityTest::new(crates![crate core {
trait A<'b> { }
impl<'b> A<'b> for u32 { }
trait WellFormed where for<'b> u32: A<'b> { }
}])
.skip_execute()
.ok()
}
Source location: tests/borrowck.rs:131 (all coverage from this test)
fn foo() -> Datum {
let x: Datum = Datum { value: 0_u32 };
let y: Datum = x;
x = Datum { value: 1_u32 };
let z: Datum = x;
return z;
}
Source location: tests/borrowck.rs:207 (all coverage from this test)
fn foo() -> u32 {
let x: u32;
if true {
x = 1_u32;
} else {
x = 2_u32;
}
return x;
}
Source location: tests/borrowck.rs:233 (all coverage from this test)
fn foo() -> u32 {
let x: u32 = 1_u32;
if true {
x = 2_u32;
}
return x;
}
Source location: tests/borrowck.rs:337 (all coverage from this test)
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1> {
if true {
let b: &'r1 mut u8 = &'r0 mut *a;
return b;
}
return a;
}
}
Source location: tests/borrowck.rs:412 (all coverage from this test)
fn foo() -> Datum {
let x: Pair = Pair {
first: Datum { value: 1_u32 },
second: Datum { value: 2_u32 },
};
let a: Datum = x.first;
let b: Datum = x.second;
return b;
}
Source location: tests/borrowck.rs:2158 (all coverage from this test)
fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
exists<'r0, 'r1> {
let n: &'r0 mut Map = &'r0 mut *m;
if true {
return n;
} else {
let o: &'r1 mut Map = &'r1 mut *m;
return o;
}
}
}
Source location: tests/borrowck.rs:2263 (all coverage from this test)
fn foo() -> i32 {
exists<'r0, 'r1> {
let result: i32;
{
let v1: i32 = 22_i32;
let v2: &'r0 i32 = &'r1 v1;
result = *v2;
}
return result;
}
}
Source location: tests/borrowck.rs:2378 (all coverage from this test)
fn min_problem_case_3<'a>(m: &'a mut Map) -> &'a mut Map {
exists<'r0, 'r1> {
let n: &'r0 mut Map = &'r0 mut *m;
if true {
} else {
}
let o: &'r1 mut Map = &'r1 mut *m;
return o;
}
}
Source location: tests/borrowck.rs:2440 (all coverage from this test)
fn foo<'a, 'b>(v1: &'a u32) -> &'b u32
where
'a: 'b,
{
exists<'r0> {
let v2: &'r0 u32 = v1;
return v2;
}
}
Source location: tests/borrowck.rs:2457 (all coverage from this test)
fn foo<'a, 'b, 'c>(v1: &'a u32) -> &'c u32
where
'a: 'b,
'b: 'c,
{
return v1;
}
Source location: tests/borrowck.rs:2499 (all coverage from this test)
fn min_problem_case_4<'a>(list: &'a mut Map, list2: &'a mut Map) -> u32 {
exists<'r0> {
let num: &'r0 mut u32 = &'r0 mut (*list).value;
list = &'a mut *list2;
num;
return 0_u32;
}
}
Source location: tests/borrowck.rs:2635 (all coverage from this test)
fn foo () -> u32 {
exists<'l_p, 'l_q, 'loan_0, 'loan_1, 'loan_2, 'loan_3> {
let a: u32 = 0_u32;
let b: u32 = 0_u32;
// In Rustc, the 1-tuple is needed for some reason
// Niko does not 100% understand, else rustc is able to
// see that this program is safe.
let q: &'l_q mut u32 = &'loan_0 mut a;
let p: &'l_p mut u32 = &'loan_1 mut a;
if true {
p = &'loan_1 mut a;
q = &'loan_2 mut b;
} else {
p = &'loan_3 mut b;
}
*q = 1_u32;
return *p;
}
}
Source location: tests/borrowck.rs:2828 (all coverage from this test)
fn foo() -> u32 {
exists<'r0, 'r1> {
'a: loop {
let x: i32 = 0_i32;
let r: &'r0 i32 = &'r1 x;
let _y: i32 = *r;
continue 'a;
}
}
}
Source location: tests/borrowck.rs:2856 (all coverage from this test)
fn foo() -> () {
'a: {
{
let 'a: v: i32 = 0_i32;
}
}
}
Source location: tests/borrowck.rs:2960 (all coverage from this test)
fn foo<'a>(m: &'a mut Map) -> &'a mut Map {
exists<'r0, 'r1> {
let n: &'r0 mut Map = &'r0 mut *m;
if false {
return n;
} else {
let o: &'r1 mut Map = &'r1 mut *m;
return o;
}
}
}
Source location: tests/borrowck.rs:3065 (all coverage from this test)
fn foo<'a>(a: &'a u32) -> &'a u32 {
exists<'r0> {
let r: &'r0 u32 = identity::<&'r0 u32>(a);
return r;
}
}
Source location: tests/borrowck.rs:3087 (all coverage from this test)
fn bar() -> u32 {
exists<'r1> {
let v: u32 = 7_u32;
let r: u32 = foo::<'r1>(&'r1 v);
return r;
}
}
Source location: tests/borrowck.rs:3117 (all coverage from this test)
fn foo<'a, 'b>(a: &'a u32) -> &'b u32
where
'a: 'b,
{
let r: &'b u32 = identity::<&'b u32>(a);
return r;
}
Source location: tests/borrowck.rs:3165 (all coverage from this test)
fn foo<'b>(a: &'b u32) -> &'b u32 {
let r: &'b u32 = bar::<'b, &'b u32>(a);
return r;
}
Source location: tests/borrowck.rs:3186 (all coverage from this test)
fn bar() -> u32 {
exists<'r0, 'r1> {
let v: u32 = 1_u32;
let p: &'r0 u32 = &'r1 v;
foo(0_u32);
return *p;
}
}
Source location: tests/borrowck.rs:3240 (all coverage from this test)
fn foo() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let p: Point = Point { x: 0_u32, y: 0_u32 };
let b1: &'r0 mut u32 = &'r1 mut p.x;
let b2: &'r2 mut u32 = &'r3 mut p.y;
*b1 = 1_u32;
*b2 = 2_u32;
return 0_u32;
}
}
Source location: tests/borrowck.rs:3362 (all coverage from this test)
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
if true {
let b: &'r1 mut u8 = &'r0 mut *a;
return b;
} else { }
let c: &'r3 mut u8 = &'r2 mut *a;
return c;
}
}
Source location: tests/borrowck.rs:3387 (all coverage from this test)
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
// This creates an outlives constraint
let b: &'r1 mut u8 = &'r0 mut *a;
if true {
return b;
} else {
// this means the loan remains live
}
// If the outlives constraint propagated here,
// we would get an error.
let c: &'r3 mut u8 = &'r2 mut *a;
return c;
}
}
Source location: tests/borrowck.rs:3436 (all coverage from this test)
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: &'r1 mut u8 = &'r0 mut *a;
return b;
let c: &'r3 mut u8 = &'r2 mut *a;
return c;
}
}
Source location: tests/borrowck.rs:3456 (all coverage from this test)
fn reborrow<'a>(a: &'a mut u8) -> &'a mut u8 {
exists<'r0, 'r1, 'r2, 'r3> {
if true {
let b: &'r1 mut u8 = &'r0 mut *a;
return b;
} else {
let c: &'r3 mut u8 = &'r2 mut *a;
return c;
}
}
}
Source location: tests/borrowck.rs:3524 (all coverage from this test)
fn foo() -> u32 {
exists<'r0, 'r1, 'r2> {
let x: u32 = 22_u32;
let p: &'r1 u32 = &'r0 x;
let q: &'r2 u32 = p;
x = 1_u32;
return 0_u32;
}
}
Source location: tests/borrowck.rs:3689 (all coverage from this test)
fn foo<'a, 'b>(p: &'a mut u32) -> u32 where 'a: 'b {
let q: &'b mut u32 = &'b mut *p;
q;
return 0 _ u32;
}
Source location: tests/borrowck.rs:3808 (all coverage from this test)
fn remove_last_node_recursive<'a>(node: &'a mut List) -> u32 {
exists<'r0> {
let next: &'r0 mut List = next_of::<'r0>(&'r0 mut *node);
if true {
remove_last_node_recursive::<'r0>(next);
} else {
*node = List { value: 0_u32 };
}
return 0_u32;
}
}
Source location: tests/borrowck.rs:3855 (all coverage from this test)
fn remove_last_node_iterative<'a>(node: &'a mut List) -> u32 {
exists<'r0, 'r1> {
let cursor: &'r0 mut List = &'r0 mut *node;
'l: loop {
let next: &'r1 mut List = &'r1 mut *cursor;
if true {
cursor = next;
} else {
break 'l;
}
}
*cursor = List { value: 0_u32 };
return 0_u32;
}
}
Source location: tests/borrowck.rs:3917 (all coverage from this test)
fn no_control_flow() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: X = X { value: 0_u32 };
let p: &'r0 mut X = &'r1 mut b;
'l: loop {
let now: &'r2 mut X = &'r2 mut *p;
if true {
let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
p = next;
} else {
break 'l;
}
}
return 0_u32;
}
}
Source location: tests/borrowck.rs:3967 (all coverage from this test)
fn conditional() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: X = X { value: 0_u32 };
let p: &'r0 mut X = &'r1 mut b;
'l: loop {
let now: &'r2 mut X = &'r2 mut *p;
if true {
if true {
let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
p = next;
} else {
}
} else {
break 'l;
}
}
return 0_u32;
}
}
Source location: tests/borrowck.rs:4056 (all coverage from this test)
fn conditional_with_indirection() -> u32 {
exists<'r0, 'r1, 'r2, 'r3> {
let b: X = X { value: 0_u32 };
let p: &'r0 mut X = &'r1 mut b;
'l: loop {
let now: &'r2 mut X = &'r2 mut *p;
if true {
if true {
let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *p);
p = next;
} else {
}
} else {
break 'l;
}
}
return 0_u32;
}
}
Source location: tests/borrowck.rs:4108 (all coverage from this test)
fn to_refs<'a>(list: &'a mut List) -> &'a mut u32 {
exists<'r0, 'r1> {
let result: &'a mut u32;
'l: loop {
result = &'r0 mut (*list).value;
if true {
let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
list = n;
} else {
return result;
}
}
}
}
Source location: tests/borrowck.rs:4143 (all coverage from this test)
fn to_refs2<'a>(list: &'a mut List) -> &'a mut u32 {
exists<'r0, 'r1> {
let result: &'a mut u32;
'l: loop {
result = &'r0 mut (*list).value;
if true {
let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
list = n;
} else {
break 'l;
}
}
return result;
}
}
Source location: tests/borrowck.rs:4190 (all coverage from this test)
fn to_refs3<'a>(list: &'a mut List) -> &'a mut u32 {
exists<'r0, 'r1> {
let result: &'a mut u32;
let cursor: &'a mut List = &'a mut *list;
'l: loop {
result = &'r0 mut (*cursor).value;
if true {
let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*cursor).next);
cursor = n;
} else {
return result;
}
}
}
}
Source location: tests/borrowck.rs:4233 (all coverage from this test)
fn next<'a>(d: &'a mut Decoder) -> &'a u32 {
exists<'r0, 'r1> {
'l: loop {
let buf: &'r0 u32 = fill_buf::<'r0>(&'r0 mut (*d).buf_read);
let s: &'r1 u32 = decode::<'r1>(buf);
if true {
return s;
} else {
}
}
}
}
Source location: tests/borrowck.rs:4356 (all coverage from this test)
fn next<'s>(f: &'s mut Filter) -> &'s mut u32 {
exists<'r0, 'r1, 'r2> {
'l: loop {
let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter);
if true {
let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item);
if keep {
return item;
} else {
}
} else {
break 'l;
}
}
return no_item::<'s>();
}
}
Source location: tests/borrowck.rs:4472 (all coverage from this test)
fn use_it<'a, 'b>() -> u32 {
exists<'r0> {
let v: Invariant<'r0> = create_invariant::<'r0>();
if true {
return sink::<'a, 'r0>(v);
} else {
return sink::<'b, 'r0>(v);
}
}
}
Source location: tests/borrowck.rs:4537 (all coverage from this test)
fn use_it_but_its_the_same_region<'a, 'b>() -> u32 where 'a: 'b, 'b: 'a {
exists<'r0> {
let v: Invariant<'r0> = create_invariant::<'r0>();
if true {
return sink::<'a, 'r0>(v);
} else {
return sink::<'b, 'r0>(v);
}
}
}
Source location: tests/codegen.rs:11 (all coverage from this test)
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:24 (all coverage from this test)
fn main() -> () {
println!(1_i32);
println!(true);
println!(false);
}
Source location: tests/codegen.rs:36 (all coverage from this test)
fn main() -> () {
let x: i32 = 42_i32;
println!(x);
}
Source location: tests/codegen.rs:49 (all coverage from this test)
fn main() -> () {
let x: i32 = 1_i32;
x = 2 _ i32;
println!(x);
}
Source location: tests/codegen.rs:64 (all coverage from this test)
fn main() -> () {
let y: i32 = add_one(1_i32);
println!(y);
}
Source location: tests/codegen.rs:79 (all coverage from this test)
fn main() -> () {
let y: i32 = identity::<i32>(42_i32);
println!(y);
}
Source location: tests/codegen.rs:95 (all coverage from this test)
fn main() -> () {
let x: i32 = 1_i32;
if true {
println!(x);
} else {
println!(0_i32);
}
}
Source location: tests/codegen.rs:110 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
println!(x);
break 'a;
}
}
Source location: tests/codegen.rs:127 (all coverage from this test)
fn main() -> () {
{
let x: i32 = 99_i32;
println!(x);
}
exists<'a> {
println!(1_i32);
}
}
Source location: tests/codegen.rs:141 (all coverage from this test)
fn main() -> () {
let p: Pair = Pair { x: 10_i32, y: 20_i32 };
println!(p.x);
println!(p.y);
}
Source location: tests/codegen.rs:171 (all coverage from this test)
fn main() -> () {
let a: usize = 100_usize;
let b: isize = 200_isize;
println!(a);
println!(b);
}
Source location: tests/codegen.rs:188 (all coverage from this test)
fn main() -> () {
let a: i32 = f(1_i32);
let b: i32 = f(2_i32);
let c: i32 = f(3_i32);
println!(a);
println!(b);
println!(c);
}
Source location: tests/codegen.rs:201 (all coverage from this test)
fn main() -> () {
let y: i32 = f(f(42_i32));
println!(y);
}
Source location: tests/codegen.rs:218 (all coverage from this test)
fn main() -> () {
let r: i32 = outer(7_i32);
println!(r);
}
Source location: tests/codegen.rs:238 (all coverage from this test)
fn main() -> () {
a();
}
Source location: tests/codegen.rs:251 (all coverage from this test)
fn main() -> () {
let r: i32 = first::<i32, bool>(10_i32, true);
println!(r);
}
Source location: tests/codegen.rs:264 (all coverage from this test)
fn main() -> () {
let w: Wrapper<i32> = Wrapper::<i32> { val: 42_i32 };
println!(w.val);
}
Source location: tests/codegen.rs:318 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
if true {
println!(x);
break 'a;
} else {
continue 'a;
}
}
}
Source location: tests/codegen.rs:336 (all coverage from this test)
fn main() -> () {
'outer: loop {
println!(1_i32);
'inner: loop {
println!(2_i32);
break 'outer;
}
}
println!(3_i32);
}
Source location: tests/codegen.rs:356 (all coverage from this test)
fn main() -> () {
'a: loop {
if true {
println!(1_i32);
break 'a;
} else {
println!(2_i32);
break 'a;
}
}
println!(3_i32);
}
Source location: tests/codegen.rs:377 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
if false {
x = 1_i32;
break 'a;
} else {
x = 2_i32;
break 'a;
}
}
println!(x);
}
Source location: tests/codegen.rs:443 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
x = 77_i32;
break 'a;
}
println!(x);
}
Source location: tests/codegen.rs:461 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
{
x = 88_i32;
break 'a;
}
}
println!(x);
}
Source location: tests/codegen.rs:477 (all coverage from this test)
fn main() -> () {
'a: {
println!(1_i32);
break 'a;
println!(2_i32);
}
println!(3_i32);
}
Source location: tests/coherence_orphan.rs:85 (all coverage from this test)
#[test]
fn mirror_FooStruct() {
FormalityTest::new(crates![crate core {
trait CoreTrait {}
trait Mirror {
type Assoc : [];
}
impl<T> Mirror for T {
type Assoc = T;
}
},
crate foo {
struct FooStruct {}
impl CoreTrait for <FooStruct as Mirror>::Assoc {}
}])
.skip_execute()
.ok()
}
Source location: tests/coherence_orphan.rs:99 (all coverage from this test)
#[test]
fn covered_VecT() {
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
struct Vec<T> {}
},
crate foo {
struct FooStruct {}
impl<T> CoreTrait<FooStruct> for Vec<T> {}
}])
.skip_execute()
.ok()
}
Source location: tests/coherence_orphan.rs:221 (all coverage from this test)
#[test]
fn CoreTraitLocal_for_AliasToKnown_in_Foo() {
// TODO: see comment in `orphan_check` from prev commit
FormalityTest::new(crates![crate core {
trait CoreTrait<T> {}
trait Unit {
type Assoc : [];
}
impl<T> Unit for T {
type Assoc = ();
}
},
crate foo {
struct FooStruct {}
impl CoreTrait<FooStruct> for <() as Unit>::Assoc {}
}])
.skip_execute()
.ok()
}
Source location: tests/coherence_overlap.rs:148 (all coverage from this test)
#[test]
fn neg_CoreTrait_for_CoreStruct_implies_no_overlap() {
FormalityTest::new(crates![crate core {
#![feature(negative_impls)]
trait CoreTrait {}
struct CoreStruct {}
impl !CoreTrait for CoreStruct {}
},
crate foo {
trait FooTrait {}
impl<T> FooTrait for T where T: CoreTrait {}
impl FooTrait for CoreStruct {}
}])
.skip_execute()
.ok()
}
Source location: tests/coherence_overlap.rs:207 (all coverage from this test)
#[test]
fn u32_T_where_T_Not_impls() {
FormalityTest::new(crates![crate core {
trait Foo {}
impl Foo for u32 {}
impl<T> Foo for T where T: Not {}
trait Not {}
}])
.skip_execute()
.ok()
}
Source location: tests/coherence_overlap.rs:308 (all coverage from this test)
#[test]
fn is_local_unknowable_trait_ref() {
FormalityTest::new(crates![crate core {
trait Project {
type Assoc: [];
}
impl<T> Project for T {
type Assoc = T;
}
trait Foo<U> { }
},
crate foo {
struct LocalType {}
trait Overlap<U> {}
impl<T, U> Overlap<U> for T
where
<T as Project>::Assoc: Foo<U> {}
impl<T> Overlap<LocalType> for () {}
}])
.skip_execute()
.ok()
}
Source location: tests/const_generics_rv_tsv_parse.rs:12 (all coverage from this test)
#[test]
fn parse_minirust_22() {
FormalityTest::new(crates![crate Foo {
trait Trait<const N> where type_of_const N is usize {}
impl Trait<usize(22)> for u32 {}
}])
.skip_execute()
.rustc_ok()
.ok()
}
Source location: tests/consts.rs:11 (all coverage from this test)
#[test]
fn nonsense_rigid_const_bound() {
FormalityTest::new(crates![crate Foo {
// This where-clause is not *provable*, but it is well-formed.
trait Foo where type_of_const true is u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:23 (all coverage from this test)
#[test]
fn ok() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool {}
trait Bar<const C> where type_of_const C is u32 {}
impl<const C> Foo<C> for u32 where type_of_const C is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:49 (all coverage from this test)
#[test]
fn holds() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool {}
impl Foo<true> for u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:58 (all coverage from this test)
#[test]
fn rigid_const_bound() {
FormalityTest::new(crates![crate Foo {
trait Foo where type_of_const true is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:92 (all coverage from this test)
#[test]
fn generic_match() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool {}
// Here, the impl matches the trait bound.
impl<const C> Foo<C> for u32 where type_of_const C is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:101 (all coverage from this test)
#[test]
fn multiple_type_of_const() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where type_of_const C is bool, type_of_const C is u32 {}
}])
.skip_execute()
.ok()
}
Source location: tests/decl_safety.rs:13 (all coverage from this test)
#[test]
fn unsafe_trait() {
FormalityTest::new(crates![crate baguette {
unsafe trait Foo {}
unsafe impl Foo for u32 {}
}])
.skip_execute()
.rustc_ok()
.ok()
}
Source location: tests/decl_safety.rs:24 (all coverage from this test)
#[test]
fn safe_trait() {
FormalityTest::new(crates![crate baguette {
safe trait Foo {}
safe impl Foo for u32 {}
}])
.skip_execute()
.rustc_ok()
.ok()
}
Source location: tests/decl_safety.rs:36 (all coverage from this test)
#[test]
fn unsafe_trait_negative_impl() {
FormalityTest::new(crates![crate baguette {
#![feature(negative_impls)]
unsafe trait Foo {}
impl !Foo for u32 {}
}])
.skip_execute()
.rustc_ok()
.ok()
}
Source location: tests/drop.rs:20 (all coverage from this test)
#[test]
fn drop_impl_simple_struct() {
FormalityTest::new(crates![
crate Foo {
struct MyStruct {
value: u32,
}
impl Drop for MyStruct {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:38 (all coverage from this test)
#[test]
fn drop_impl_generic_struct() {
FormalityTest::new(crates![
crate Foo {
trait Clone {}
struct MyStruct<T> where T: Clone {
value: T,
}
impl<T> Drop for MyStruct<T> where T: Clone {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:54 (all coverage from this test)
#[test]
fn drop_impl_generic_no_where_clauses() {
FormalityTest::new(crates![
crate Foo {
struct Wrapper<T> {
value: T,
}
impl<T> Drop for Wrapper<T> {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:78 (all coverage from this test)
#[test]
fn drop_impl_subset_where_clauses() {
FormalityTest::new(crates![
crate Foo {
trait Clone {}
trait Debug {}
struct MyStruct<T> where T: Clone, T: Debug {
value: T,
}
// Impl has no where-clauses — but the struct requires them.
impl<T> Drop for MyStruct<T> {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:94 (all coverage from this test)
#[test]
fn drop_impl_enum() {
FormalityTest::new(crates![
crate Foo {
enum MyEnum {
Variant{},
}
impl Drop for MyEnum {}
}
])
.skip_execute()
.ok()
}
Source location: tests/drop.rs:111 (all coverage from this test)
#[test]
fn drop_impl_cross_crate_local() {
FormalityTest::new(crates![
crate a {
struct MyStruct {
value: u32,
}
impl Drop for MyStruct {}
},
crate b {}
])
.skip_execute()
.ok()
}
Source location: tests/field_projections.rs:17 (all coverage from this test)
fn test(ptr: Ptr) -> () {
let x: () = *ptr;
}
Source location: tests/functions.rs:25 (all coverage from this test)
Source location: tests/functions.rs:39 (all coverage from this test)
Source location: tests/mir_typeck.rs:14 (all coverage from this test)
fn foo (v1: u32) -> u32 {
return v1;
}
Source location: tests/mir_typeck.rs:37 (all coverage from this test)
fn foo () -> u8 {
let v1: u16 = 5_u16;
let v2: u32 = 5_u32;
let v3: u64 = 5_u64;
let v4: usize = 5_usize;
let v5: i8 = 5_i8;
let v6: i16 = 5_i16;
let v7: i32 = 5_i32;
let v8: i64 = 5_i64;
let v9: isize = 5_isize;
let v10: bool = false;
return 5_u8;
}
Source location: tests/mir_typeck.rs:93 (all coverage from this test)
fn foo (v1: u32) -> u32 {
return v1;
}
Source location: tests/mir_typeck.rs:110 (all coverage from this test)
fn foo() -> u32 {
let v0: u32 = 0_u32;
loop {
v0 = v0;
}
}
Source location: tests/mir_typeck.rs:123 (all coverage from this test)
fn foo () -> bool {
return true;
}
Source location: tests/mir_typeck.rs:140 (all coverage from this test)
fn foo (b: bool) -> u32 {
if b {
return 1_u32;
} else {
return 2_u32;
}
}
Source location: tests/mir_typeck.rs:193 (all coverage from this test)
fn bar(v1: u32) -> u32 {
let v0: u32 = foo(v1);
return v0;
}
Source location: tests/mir_typeck.rs:214 (all coverage from this test)
fn foo (v1: u32) -> u32 {
return v1;
}
Source location: tests/mir_typeck.rs:259 (all coverage from this test)
fn foo (v1: u32) -> u32 {
let v2: Dummy = Dummy { value: 1_u32, is_true: false };
v2.value = 2_u32;
return v1;
}
Source location: tests/mir_typeck.rs:276 (all coverage from this test)
fn foo() -> () {
let s1: S1<u8>;
}
Source location: tests/mir_typeck.rs:439 (all coverage from this test)
fn bar(v1: u32) -> u32 {
let v0: u32 = identity::<u32>(v1);
return v0;
}
Source location: tests/mir_typeck.rs:899 (all coverage from this test)
fn foo() -> bool {
let v1: bool = false;
return v1;
}
Source location: tests/mir_typeck.rs:923 (all coverage from this test)
fn foo<'a>(v1: &'a u32) -> &'a u32 {
exists<'r0> {
let v2: &'r0 u32 = v1;
return v2;
}
}
Source location: tests/mir_typeck.rs:941 (all coverage from this test)
fn foo () -> u32 {
exists<'a> {
let v0: u32 = 0_u32;
let v1: &'a u32 = &'a v0;
let v2: u32 = *v1;
return v2;
}
}
Source location: tests/mir_typeck.rs:961 (all coverage from this test)
fn foo<'a, T>(v1: &'a T) -> T
where
T: Copy,
T: 'a,
{
exists<'r0> {
let v2: T = *v1;
return v2;
}
}
Source location: tests/mir_typeck.rs:988 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
break 'a;
}
return 0_u32;
}
Source location: tests/mir_typeck.rs:1047 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
continue 'a;
}
return 0_u32;
}
Source location: tests/mir_typeck.rs:1116 (all coverage from this test)
fn foo<'a>(v1: &'a Pair) -> u32 {
exists<'r0> {
let v2: u32 = (*v1).value;
return v2;
}
}
Source location: tests/mir_typeck.rs:1142 (all coverage from this test)
fn foo() -> u32 {
'a: {
break 'a;
}
return 0_u32;
}
Source location: tests/projection.rs:25 (all coverage from this test)
#[test]
fn normalize_basic() {
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> {} => { <Vec<T> as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <Vec<!ty_1> as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> {} => { Iterator(Vec<T>), <Vec<T> as Iterator>::Item = T }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T), <T as Iterator>::Item = Foo } => { <T as Iterator>::Item = Foo }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]
);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <!ty_1 as Iterator>::Item} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T) } => { <T as Iterator>::Item = <T as Iterator>::Item }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = <U as Iterator>::Item }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => Vec<<!ty_1 as Iterator>::Item>, ?ty_3 => <!ty_1 as Iterator>::Item} }}"]);
}
Source location: tests/projection.rs:31 (all coverage from this test)
#[test]
fn normalize_basic() {
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> {} => { <Vec<T> as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <Vec<!ty_1> as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> {} => { Iterator(Vec<T>), <Vec<T> as Iterator>::Item = T }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T), <T as Iterator>::Item = Foo } => { <T as Iterator>::Item = Foo }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]
);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <!ty_1 as Iterator>::Item} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T) } => { <T as Iterator>::Item = <T as Iterator>::Item }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = <U as Iterator>::Item }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => Vec<<!ty_1 as Iterator>::Item>, ?ty_3 => <!ty_1 as Iterator>::Item} }}"]);
}
Source location: tests/projection.rs:44 (all coverage from this test)
#[test]
fn normalize_basic() {
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> {} => { <Vec<T> as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <Vec<!ty_1> as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> {} => { Iterator(Vec<T>), <Vec<T> as Iterator>::Item = T }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T), <T as Iterator>::Item = Foo } => { <T as Iterator>::Item = Foo }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]
);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <!ty_1 as Iterator>::Item} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T) } => { <T as Iterator>::Item = <T as Iterator>::Item }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = <U as Iterator>::Item }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => Vec<<!ty_1 as Iterator>::Item>, ?ty_3 => <!ty_1 as Iterator>::Item} }}"]);
}
Source location: tests/projection.rs:55 (all coverage from this test)
#[test]
fn normalize_basic() {
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> {} => { <Vec<T> as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <Vec<!ty_1> as Iterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> {} => { Iterator(Vec<T>), <Vec<T> as Iterator>::Item = T }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T), <T as Iterator>::Item = Foo } => { <T as Iterator>::Item = Foo }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]
);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <!ty_1 as Iterator>::Item} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> { Iterator(T) } => { <T as Iterator>::Item = <T as Iterator>::Item }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {} }}"]);
test_where_clause(
NORMALIZE_BASIC,
"forall<T> exists<U> { Iterator(T) } => { <T as Iterator>::Item = <U as Iterator>::Item }",
).assert_ok(
expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }, Constraints { env: Env { variables: [!ty_1, ?ty_3, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => Vec<<!ty_1 as Iterator>::Item>, ?ty_3 => <!ty_1 as Iterator>::Item} }}"]);
}
Source location: tests/projection.rs:89 (all coverage from this test)
#[test]
fn normalize_into_iterator() {
test_where_clause(
NORMALIZE_INTO_ITERATOR,
"forall<T> exists<U> {} => { <Vec<T> as IntoIterator>::Item = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => <Vec<!ty_1> as IntoIterator>::Item} }, Constraints { env: Env { variables: [!ty_1, ?ty_2], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_2 => !ty_1} }}"]);
}
Source location: tests/projection.rs:112 (all coverage from this test)
#[test]
fn projection_equality() {
test_where_clause(
PROJECTION_EQUALITY,
"exists<U> {} => { Trait1(S), <S as Trait1<>>::Type = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => <S as Trait1>::Type} }}"]);
test_where_clause(PROJECTION_EQUALITY, "exists<U> {} => { Trait2(S, U) }")
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => <S as Trait1>::Type} }}"]);
}
Source location: tests/projection.rs:115 (all coverage from this test)
#[test]
fn projection_equality() {
test_where_clause(
PROJECTION_EQUALITY,
"exists<U> {} => { Trait1(S), <S as Trait1<>>::Type = U }",
)
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => <S as Trait1>::Type} }}"]);
test_where_clause(PROJECTION_EQUALITY, "exists<U> {} => { Trait2(S, U) }")
.assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => u32} }, Constraints { env: Env { variables: [?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false }, known_true: true, substitution: {?ty_1 => <S as Trait1>::Type} }}"]);
}
Source location: tests/return_validation.rs:33 (all coverage from this test)
fn foo() -> () {
}
Source location: tests/return_validation.rs:51 (all coverage from this test)
fn foo(b: bool) -> u32 {
if b {
return 1_u32;
} else {
return 2_u32;
}
}
Source location: tests/return_validation.rs:84 (all coverage from this test)
fn foo() -> u32 {
loop {
}
}
Source location: tests/return_validation.rs:118 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
break 'a;
}
return 0_u32;
}
Source location: tests/return_validation.rs:132 (all coverage from this test)
fn foo() -> u32 {
return 42_u32;
}
Source location: tests/well_formed_struct.rs:17 (all coverage from this test)
fn main() -> () {
exists<'y> {
let a: u32 = 22_u32;
let f: Foo<'y> = Foo::<'y> { y: &'y a };
}
}
Source location: tests/well_formed_trait_ref.rs:19 (all coverage from this test)
#[test]
fn dependent_where_clause() {
FormalityTest::new(crates![crate foo {
trait Trait1 {}
trait Trait2 {}
struct S1<T> where T: Trait1 {
dummy: T,
}
struct S2<T> where T: Trait1, S1<T> : Trait2 {
dummy: T,
}
}])
.skip_execute()
.ok()
}
Source location: tests/well_formed_trait_ref.rs:56 (all coverage from this test)
#[test]
fn lifetime_param() {
FormalityTest::new(crates![crate foo {
trait Trait1<'a> {}
struct S1 {}
struct S2<'a> where S1: Trait1<'a> {}
}])
.skip_execute()
.ok()
}
Source location: tests/well_formed_trait_ref.rs:71 (all coverage from this test)
#[test]
fn static_lifetime_param() {
FormalityTest::new(crates![crate foo {
trait Trait1<'a> {}
struct S1 {}
impl Trait1<'static> for S1 {}
struct S2 where S1: Trait1<'static> {}
}])
.skip_execute()
.ok()
}
Source location: tests/well_formed_trait_ref.rs:86 (all coverage from this test)
#[test]
fn const_param() {
FormalityTest::new(crates![crate foo {
trait Trait1<const C> where type_of_const C is u32 {}
struct S1 {}
impl Trait1<u32(3)> for S1 {}
struct S2 where S1: Trait1<u32(3)> {}
}])
.skip_execute()
.ok()
}