Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: prove_wf / tuples

tuples
LineCoverageSource
52✗(for_all(decls, env, assumptions, parameters, &prove_wf_recursive) => c)
──────── ("tuples")
5436(prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Tuple(_), parameters }) => c)

36 tests exercised this rule:

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{},
}
Proof tree

Source location: tests/basic_tests.rs:356

fn a() -> () { trusted }
}])
p_execute()
);
}

#[test]
_impl_dup() {
alityTest::new(crates![crate core {
trait MyTrait {}
struct MyStruct {}
impl MyTrait for MyStruct {}
impl MyTrait for MyStruct {}
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  `impl MyTrait for MyStruct { }` is defined multiple times"#]]);
}

#[test]
_neg_impl_dup() {
alityTest::new(crates![crate core {
trait MyTrait {}
struct MyStruct {}
impl !MyTrait for MyStruct {}
impl !MyTrait for MyStruct {}
}])
(expect_test::expect![[r#"
the rule "check crate" at (mod.rs) failed because
  `impl ! MyTrait for MyStruct {}` is defined multiple times"#]]);
}

#[test]
missing_required_fn() {
alityTest::new(crates![crate core {
trait Foo {
    fn bar(self_: u32) -> u32;
}
Proof tree

Source location: tests/borrowck.rs:2628

fn foo() -> () {
    'a: {
        {
            let 'a: v: i32 = 0 _ i32;
        }
    }
}
Proof tree
… (200 of 1015 nodes shown)

Source location: tests/codegen.rs:11

fn main() -> () {
    println!(22 _ i32);
}
Proof tree
… (200 of 989 nodes shown)

Source location: tests/codegen.rs:24

fn main() -> () {
    println!(1 _ i32);
    println!(true);
    println!(false);
}
Proof tree
… (200 of 995 nodes shown)

Source location: tests/codegen.rs:36

fn main() -> () {
    let x: i32 = 42 _ i32;
    println!(x);
}
Proof tree
… (200 of 1013 nodes shown)

Source location: tests/codegen.rs:49

fn main() -> () {
    let x: i32 = 1 _ i32;
    x = 2 _ i32;
    println!(x);
}
Proof tree
… (200 of 1025 nodes shown)

Source location: tests/codegen.rs:64

fn main() -> () {
    let y: i32 = add_one(1 _ i32);
    println!(y);
}
Proof tree
… (200 of 1060 nodes shown)

Source location: tests/codegen.rs:79

fn main() -> () {
    let y: i32 = identity::<i32>(42 _ i32);
    println!(y);
}
Proof tree
… (200 of 1060 nodes shown)

Source location: tests/codegen.rs:95

fn main() -> () {
    let x: i32 = 1 _ i32;
    if true {
        println!(x);
    } else {
        println!(0 _ i32);
    }
}
Proof tree
… (200 of 1031 nodes shown)

Source location: tests/codegen.rs:110

fn main() -> () {
    let x: i32 = 0 _ i32;
    'a: loop {
        println!(x);
        break 'a;
    }
}

Proof trees omitted for the remaining 26 tests.

Source location: tests/codegen.rs:127

fn main() -> () {
    {
        let x: i32 = 99 _ i32;
        println!(x);
    }
    exists<'a> {
        println!(1 _ i32);
    }
}

Source location: tests/codegen.rs:141

fn main() -> () {
    let p: Pair = Pair { x: 10 _ i32, y: 20 _ i32 };
    println!(p.x);
    println!(p.y);
}

Source location: tests/codegen.rs:171

fn main() -> () {
    let a: usize = 100 _ usize;
    let b: isize = 200 _ isize;
    println!(a);
    println!(b);
}

Source location: tests/codegen.rs:188

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

fn main() -> () {
    let y: i32 = f(f(42 _ i32));
    println!(y);
}

Source location: tests/codegen.rs:218

fn main() -> () {
    let r: i32 = outer(7 _ i32);
    println!(r);
}

Source location: tests/codegen.rs:238

fn main() -> () {
    a();
}

Source location: tests/codegen.rs:251

fn main() -> () {
    let r: i32 = first::<i32, bool>(10 _ i32, true);
    println!(r);
}

Source location: tests/codegen.rs:264

fn main() -> () {
    let w: Wrapper<i32> = Wrapper::<i32> { val: 42 _ i32 };
    println!(w.val);
}

Source location: tests/codegen.rs:318

fn main() -> () {
    let x: i32 = 0 _ i32;
    'a: loop {
        if true {
            println!(x);
            break 'a;
        } else {
            continue 'a;
        }
    }
}

Source location: tests/codegen.rs:336

fn main() -> () {
    'outer: loop {
        println!(1 _ i32);
        'inner: loop {
            println!(2 _ i32);
            break 'outer;
        }
    }
    println!(3 _ i32);
}

Source location: tests/codegen.rs:356

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

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

fn main() -> () {
    let x: i32 = 0 _ i32;
    'a: loop {
        x = 77 _ i32;
        break 'a;
    }
    println!(x);
}

Source location: tests/codegen.rs:461

fn main() -> () {
    let x: i32 = 0 _ i32;
    'a: loop {
        {
            x = 88 _ i32;
            break 'a;
        }
    }
    println!(x);
}

Source location: tests/codegen.rs:477

fn main() -> () {
    'a: {
        println!(1 _ i32);
        break 'a;
        println!(2 _ i32);
    }
    println!(3 _ i32);
}

Source location: tests/coherence_orphan.rs:196

#[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/field_projections.rs:17

fn test(ptr: Ptr) -> () {
    let x: () = *ptr;
}

Source location: tests/functions.rs:24

Source location: tests/functions.rs:37

Source location: tests/mir_typeck.rs:250

fn foo() -> () {
    let s1: S1<u8>;
}

Source location: tests/references.rs:36

Source location: tests/return_validation.rs:31

fn foo() -> () {
}

Source location: tests/traits.rs:13

Source location: tests/well_formed_struct.rs:17

fn main() -> () {
    exists<'y> {
        let a: u32 = 22 _ u32;
        let f: Foo<'y> = Foo::<'y> { y: &'y a };
    }
}