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: check_fn_body / trusted fn body

trusted fn body
LineCoverageSource
──────── ("trusted fn body")
8312(check_fn_body(program, env, assumptions, MaybeFnBody::FnBody(FnBody::TrustedFnBody), input_args, output_ty) => ())

12 tests exercised this rule:

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

Source location: tests/basic_tests.rs:356 (all coverage from this test)

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]
items_with_duplicate_fn_names() {
alityTest::new(crates![crate core {
trait Foo {
    fn bar(self_: u32) -> u32;
}
Proof tree

Source location: tests/basic_tests.rs:457 (all coverage from this test)

Proof tree

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;
            }
        }
    }
}
Proof tree
… (200 of 1733 nodes shown)

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;
    }
}
Proof tree
… (200 of 2021 nodes shown)

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;
            }
        }
    }
}
Proof tree
… (200 of 1888 nodes shown)

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 {
            }
        }
    }
}
Proof tree
… (200 of 1596 nodes shown)

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>();
    }
}
Proof tree
… (200 of 2783 nodes shown)

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);
        }
    }
}
Proof tree
… (200 of 1182 nodes shown)

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);
        }
    }
}
Proof tree
… (200 of 1190 nodes shown)

Source location: tests/functions.rs:25 (all coverage from this test)

Proof trees omitted for the remaining 2 tests; each one is on its test’s page in Coverage by test.

Source location: tests/functions.rs:39 (all coverage from this test)