Test foo
Source location: tests/basic_tests.rs:121
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{},
}
Rules proved (32)
Premises failed (0)
This test records no negative coverage.
Proof trees
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 (feature gate)mod.rs:224args
for_allmod.rs:72args
check_crate_item (trait)mod.rs:188args
check_trait (check trait)traits.rs:26args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait well formed)prove_wc.rs:135args
for_allcombinators.rs:69prove_wf (universal variables)prove_wf.rs:27args
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
for_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 (free fn)mod.rs:207args
check_free_fn (check free fn)fns.rs:25args
check_fn (check fn)fns.rs:56args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (forall)prove_wc.rs:36args
prove_wc (trait well formed)prove_wc.rs:135args
for_allcombinators.rs:69prove_wf (integers and booleans)prove_wf.rs:56args
for_allcombinators.rs:69prove_wf (universal variables)prove_wf.rs:27args
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 (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
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 (parameter well formed)prove_wc.rs:154args
prove_wf (tuples)prove_wf.rs:50args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args
check_fn_body (trusted fn body)fns.rs:82args
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_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
check_safety_matches (safety matches)impls.rs:85args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:340args
check_coherence (check_coherence)coherence.rs:24args
for_allcoherence.rs:8for_allcoherence.rs:17args
for_allcoherence.rs:8for_allcoherence.rs:18args
overlap_check (skip_same_impl)coherence.rs:75
for_allcoherence.rs:8for_allcoherence.rs:20args
orphan_check (orphan_check)coherence.rs:39args
prove_wc_list (some)prove_wc_list.rs:28args
prove_wc (trait ref is local)prove_wc.rs:141args
is_local_trait_ref (local trait)is_local.rs:208args
prove_after (prove_after)prove_after.rs:20args
prove_wc_list (none)prove_wc_list.rs:21args