Positive coverage: check_fn_body / no fn body
no fn body| Line | Coverage | Source |
|---|---|---|
| ──────── ("no fn body") | ||
| 76 | 192 | (check_fn_body(program, env, assumptions, MaybeFnBody::NoFnBody, input_args, output_ty) => ()) |
192 tests exercised this rule:
Source location: src/test_util.rs:423 (all coverage from this test)
#[test]
fn borrowck_ok_checks_rustc_ok_once() {
let before = rustc_runs();
FormalityTest::new(ACCEPTED)
.rustc_ok()
.skip_execute()
.borrowck_ok();
assert_eq!(rustc_runs() - before, 1);
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: src/test_util.rs:434 (all coverage from this test)
#[test]
#[should_panic(expected = "expected `rustc` to fail but it succeeded")]
fn borrowck_ok_enforces_rustc_err() {
FormalityTest::new(ACCEPTED)
.rustc_err(expect_test::expect![[r#"..."#]])
.skip_execute()
.borrowck_ok();
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: src/test_util.rs:516 (all coverage from this test)
#[test]
fn rustc_expectation_is_independent_of_borrowck_modes() {
let before = rustc_runs();
FormalityTest::new(NLL_ONLY_ERROR)
.rustc_err(expect_test::expect![[r#"
error[E0499]: cannot borrow `*m` as mutable more than once at a time
--> lib.rs
|
3 | pub fn foo<'a00>(mut m: &'a00 mut Map) -> &'a00 mut Map {
| ---- lifetime `'a00` defined here
4 | {
5 | let mut n: &'_ mut Map = &mut *m;
| ------- first mutable borrow occurs here
6 | if false {
7 | return n;
| - returning this value requires that `*m` is borrowed for `'a00`
8 | } else {
9 | let mut o: &'_ mut Map = &mut *m;
| ^^^^^^^ second mutable borrow occurs here
For more information about this error, try `rustc --explain E0499`.
error: could not compile `Foo` (lib) due to 1 previous error
"#]])
.borrowck_err(BorrowCheckFailure::Nll, expect_test::expect![[r#"
the rule "borrow of disjoint places" at (nll.rs) failed because
condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
&loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
&access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
the rule "loan_cannot_outlive" at (nll.rs) failed because
condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
&lifetime.upcast() = !lt_1
the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
{
Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
{
Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
Lt::Variable(Variable::ExistentialVar(_)) => true,
Lt::Variable(Variable::BoundVar(_)) =>
panic!("cannot outlive a bound var"), Lt::Erased => true,
}, Parameter::Const(_) => panic!("cannot outlive a constant"),
})`
the rule "write-indirect" at (nll.rs) failed because
pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`
the rule "write-indirect" at (nll.rs) failed because
condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
place_loaned_ref = m : &!lt_1 mut Map"#]]);
assert_eq!(rustc_runs() - before, 1);
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
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:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:23 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(10)
rowck_ok();
}
#[test]
tion_limit_skipped_execution_needs_no_steps() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.execution_step_limit(0)
.skip_execute()
.borrowck_ok();
}
#[test]
tion_limit_default_allowance_runs_small_programs() {
program = crates![crate Foo {
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program)
.expect_output("1\n")
.borrowck_ok();
}
#[test]
tion_limit_borrowck_finishes_on_last_allowed_step() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(11)
ect_output("1\n")
rowck_ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_borrowck_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
rowck_ok();
}
#[test]
_panic(expected = "program output mismatch")]
wck_checks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
rowck_ok();
}
#[test]
wck_accepts_matching_output() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("1\n")
rowck_ok();
}
#[test]
wck_skipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:35 (all coverage from this test)
fn example() -> () {}
}];
alityTest::new(program)
.execution_step_limit(0)
.skip_execute()
.borrowck_ok();
}
#[test]
tion_limit_default_allowance_runs_small_programs() {
program = crates![crate Foo {
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program)
.expect_output("1\n")
.borrowck_ok();
}
#[test]
tion_limit_borrowck_finishes_on_last_allowed_step() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(11)
ect_output("1\n")
rowck_ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_borrowck_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
rowck_ok();
}
#[test]
_panic(expected = "program output mismatch")]
wck_checks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
rowck_ok();
}
#[test]
wck_accepts_matching_output() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("1\n")
rowck_ok();
}
#[test]
wck_skipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:45 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program)
.expect_output("1\n")
.borrowck_ok();
}
#[test]
tion_limit_borrowck_finishes_on_last_allowed_step() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(11)
ect_output("1\n")
rowck_ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_borrowck_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
rowck_ok();
}
#[test]
_panic(expected = "program output mismatch")]
wck_checks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
rowck_ok();
}
#[test]
wck_accepts_matching_output() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("1\n")
rowck_ok();
}
#[test]
wck_skipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:55 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(11)
ect_output("1\n")
rowck_ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_borrowck_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
rowck_ok();
}
#[test]
_panic(expected = "program output mismatch")]
wck_checks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
rowck_ok();
}
#[test]
wck_accepts_matching_output() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("1\n")
rowck_ok();
}
#[test]
wck_skipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:65 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
rowck_ok();
}
#[test]
_panic(expected = "program output mismatch")]
wck_checks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
rowck_ok();
}
#[test]
wck_accepts_matching_output() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("1\n")
rowck_ok();
}
#[test]
wck_skipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:75 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
rowck_ok();
}
#[test]
wck_accepts_matching_output() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("1\n")
rowck_ok();
}
#[test]
wck_skipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Proof tree
check_all_crates (check all prefixes)mod.rs:55args
for_allmod.rs:42for_allmod.rs:52args
check_crate (check crate)mod.rs:76args
for_allmod.rs:61for_allmod.rs:73args
check_crate_item (trait)mod.rs:189args
check_trait (check trait)traits.rs:25args
scopetraits.rs:9prove_predicate_list (none)prove_predicate_list.rs:21args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
prove_after (prove_after)prove_after.rs:20args
prove_predicate_list (none)prove_predicate_list.rs:21args
check_safety_matches (safety matches)impls.rs:83args
check_drop_impl_always_applicable (not a Drop impl)impls.rs:342args
for_allmod.rs:73args
check_crate_item (trait impl)mod.rs:196args
check_trait_impl (check_trait_impl)impls.rs:40args
scopeimpls.rs:14prove_predicate_list (none)prove_predicate_list.rs:21args
prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (positive impl)prove_predicate.rs:79args
scopeprove_predicate.rs:22prove_predicate_list (some)prove_predicate_list.rs:28args
prove_predicate (eq)prove_predicate.rs:116args
Source location: tests/borrowck.rs:84 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
ect_output("1\n")
rowck_ok();
}
#[test]
wck_skipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Proof trees omitted for the remaining 182 tests; each one is on its test’s page in Coverage by test.
Source location: tests/borrowck.rs:96 (all coverage from this test)
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.borrowck_ok();
}
==============================================================
alization and move tracking tests
//
tests exercise the initialization/move analysis. Currently
lity does not track initialization or moves, so tests that
t errors are #[ignore]d. Tests that expect success pass today
ously, since there's no init checking to reject them).
==============================================================
of an uninitialized variable should be an error.
///
ust,ignore
oo() -> u32 {
let x: u32;
x // ERROR: x isn't initialized
/// }
/// ```
#[test]
f_uninitialized_variable() {
alityTest::new(crates![crate Foo {
fn foo() -> u32 {
let x: u32;
return x;
}
Source location: tests/borrowck.rs:214 (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:290 (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:316 (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:420 (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:495 (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:2470 (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:2575 (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:2690 (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:2768 (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:2785 (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:2827 (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:2963 (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:3156 (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:3184 (all coverage from this test)
fn foo() -> () {
'a: {
{
let 'a: v: i32 = 0_i32;
}
}
}
Source location: tests/borrowck.rs:3288 (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:3393 (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:3415 (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:3445 (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:3493 (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:3514 (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:3568 (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:3690 (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:3715 (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:3764 (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:3784 (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:3869 (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:4048 (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:4167 (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:4214 (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:4276 (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:4326 (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:4415 (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:4467 (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:4502 (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:4549 (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:4592 (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:4715 (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:4831 (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:4896 (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/borrowck.rs:4970 (all coverage from this test)
fn f() -> u32 {
exists<'r0> {
let v: u32 = 0_u32;
let w: Wrapper<'r0> = Wrapper::<'r0> { value: &'r0 v };
return *w.value;
}
}
Source location: tests/borrowck.rs:4985 (all coverage from this test)
fn foo() -> u32 {
let a: u32 = 0_u32;
a;
a;
return 0_u32;
}
Source location: tests/borrowck.rs:5004 (all coverage from this test)
fn foo() -> u32 {
exists<'l0> {
let a: u32 = 0_u32;
let p: &'l0 u32 = &'l0 a;
let q: &'l0 u32 = p;
let r: &'l0 u32 = p;
p;
return 0_u32;
}
}
Source location: tests/borrowck.rs:5022 (all coverage from this test)
fn foo() -> () {
let x: u32 = 1_u32;
exists<'r0> {
let r: &'r0 mut u32 = &'r0 mut x;
x += *r;
}
}
Source location: tests/borrowck.rs:5120 (all coverage from this test)
fn bump<'a>(p: &'a mut u32) -> () {
*p += 1_u32;
}
Source location: tests/codegen.rs:12 (all coverage from this test)
fn main() -> () {
'a: loop {}
}
Source location: tests/codegen.rs:22 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(20)
ect_output("1\n")
);
}
#[test]
tion_limit_finishes_on_last_allowed_step() {
his program currently takes 11 MiniRust steps, including MachineStop.
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(11)
ect_output("1\n")
);
}
#[test]
_panic(expected = "execution step limit reached after 10 steps")]
tion_limit_stops_when_allowance_is_too_small() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(10)
);
}
#[test]
tion_limit_skipped_execution_needs_no_steps() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.execution_step_limit(0)
.skip_execute()
.ok();
}
#[test]
tion_limit_default_allowance_runs_small_programs() {
program = crates![crate Foo {
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program).expect_output("1\n").ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
);
}
#[test]
_panic(expected = "program output mismatch")]
ecks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
);
}
#[test]
ipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:33 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(11)
ect_output("1\n")
);
}
#[test]
_panic(expected = "execution step limit reached after 10 steps")]
tion_limit_stops_when_allowance_is_too_small() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(10)
);
}
#[test]
tion_limit_skipped_execution_needs_no_steps() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.execution_step_limit(0)
.skip_execute()
.ok();
}
#[test]
tion_limit_default_allowance_runs_small_programs() {
program = crates![crate Foo {
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program).expect_output("1\n").ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
);
}
#[test]
_panic(expected = "program output mismatch")]
ecks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
);
}
#[test]
ipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:43 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(10)
);
}
#[test]
tion_limit_skipped_execution_needs_no_steps() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.execution_step_limit(0)
.skip_execute()
.ok();
}
#[test]
tion_limit_default_allowance_runs_small_programs() {
program = crates![crate Foo {
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program).expect_output("1\n").ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
);
}
#[test]
_panic(expected = "program output mismatch")]
ecks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
);
}
#[test]
ipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:55 (all coverage from this test)
fn example() -> () {}
}];
alityTest::new(program)
.execution_step_limit(0)
.skip_execute()
.ok();
}
#[test]
tion_limit_default_allowance_runs_small_programs() {
program = crates![crate Foo {
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program).expect_output("1\n").ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
);
}
#[test]
_panic(expected = "program output mismatch")]
ecks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
);
}
#[test]
ipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:63 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}];
alityTest::new(program).expect_output("1\n").ok();
}
#[test]
_panic(expected = "execution step limit reached after 0 steps")]
tion_limit_zero_allowance_prevents_execution() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
);
}
#[test]
_panic(expected = "program output mismatch")]
ecks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
);
}
#[test]
ipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:73 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
cution_step_limit(0)
);
}
#[test]
_panic(expected = "program output mismatch")]
ecks_output_expectation() {
alityTest::new(crates![crate Foo {
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
);
}
#[test]
ipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:83 (all coverage from this test)
fn main() -> () { println!(1_u32); }
}])
ect_output("999\n")
);
}
#[test]
ipped_execution_does_not_check_output() {
program = crates![crate Foo {
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:95 (all coverage from this test)
fn example() -> () {}
}];
alityTest::new(program)
.expect_output("999\n")
.skip_execute()
.ok();
}
#[test]
_world() {
alityTest::new(crates![crate test {
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:106 (all coverage from this test)
fn main() -> () {
println!(22_i32);
}
Source location: tests/codegen.rs:119 (all coverage from this test)
fn main() -> () {
println!(1_i32);
println!(true);
println!(false);
}
Source location: tests/codegen.rs:131 (all coverage from this test)
fn main() -> () {
let x: i32 = 42_i32;
println!(x);
}
Source location: tests/codegen.rs:144 (all coverage from this test)
fn main() -> () {
let x: i32 = 1_i32;
x = 2 _ i32;
println!(x);
}
Source location: tests/codegen.rs:159 (all coverage from this test)
fn main() -> () {
let y: i32 = add_one(1_i32);
println!(y);
}
Source location: tests/codegen.rs:174 (all coverage from this test)
fn main() -> () {
let y: i32 = identity::<i32>(42_i32);
println!(y);
}
Source location: tests/codegen.rs:190 (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:205 (all coverage from this test)
fn main() -> () {
let x: i32 = 0_i32;
'a: loop {
println!(x);
break 'a;
}
}
Source location: tests/codegen.rs:222 (all coverage from this test)
fn main() -> () {
{
let x: i32 = 99_i32;
println!(x);
}
exists<'a> {
println!(1_i32);
}
}
Source location: tests/codegen.rs:236 (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:251 (all coverage from this test)
fn main() -> () {
let x: i32 = 42_i32;
exists<'a> {
let r: & 'a i32 = & 'a x;
println!(*r);
}
}
Source location: tests/codegen.rs:265 (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:282 (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:295 (all coverage from this test)
fn main() -> () {
let y: i32 = f(f(42_i32));
println!(y);
}
Source location: tests/codegen.rs:312 (all coverage from this test)
fn main() -> () {
let r: i32 = outer(7_i32);
println!(r);
}
Source location: tests/codegen.rs:332 (all coverage from this test)
fn main() -> () {
a();
}
Source location: tests/codegen.rs:345 (all coverage from this test)
fn main() -> () {
let r: i32 = first::<i32, bool>(10_i32, true);
println!(r);
}
Source location: tests/codegen.rs:358 (all coverage from this test)
fn main() -> () {
let w: Wrapper<i32> = Wrapper::<i32> { val: 42_i32 };
println!(w.val);
}
Source location: tests/codegen.rs:374 (all coverage from this test)
fn main() -> () {
let p: Pair = Pair { x: 10_i32, y: 20_i32 };
exists<'a> {
let r: & 'a i32 = & 'a p.x;
println!(*r);
}
}
Source location: tests/codegen.rs:391 (all coverage from this test)
fn main() -> () {
let p: Pair = Pair { x: 10_i32, y: 20_i32 };
exists<'a> {
let r: & 'a Pair = & 'a p;
println!((*r).x);
println!((*r).y);
}
}
Source location: tests/codegen.rs:410 (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:428 (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:448 (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:469 (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:485 (all coverage from this test)
fn main() -> () {
let x: i32 = 1_i32;
exists<'a> {
let r: &'a mut i32 = &'a mut x;
*r = 2_i32;
println!(*r);
}
}
Source location: tests/codegen.rs:501 (all coverage from this test)
fn main() -> () {
let x: i32 = 42_i32;
exists<'a> {
let r1: & 'a i32 = & 'a x;
let r2: & 'a i32 = & 'a *r1;
println!(*r2);
}
}
Source location: tests/codegen.rs:516 (all coverage from this test)
fn main() -> () {
let x: i32 = 55_i32;
exists<'a> {
let r: & 'a i32 = & 'a x;
println!(*r);
}
}
Source location: tests/codegen.rs:532 (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:550 (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:566 (all coverage from this test)
fn main() -> () {
'a: {
println!(1_i32);
break 'a;
println!(2_i32);
}
println!(3_i32);
}
Source location: tests/codegen.rs:586 (all coverage from this test)
fn main() -> () {
let x: u32 = 1_u32;
exists<'a> {
let r: &'a mut u32 = &'a mut x;
let amount: u32 = update::<'a>(r);
println!(amount);
}
}
Source location: tests/codegen.rs:598 (all coverage from this test)
fn main() -> () {
let x: i32 = 1_i32 + 2_i32;
println!(x);
}
Source location: tests/codegen.rs:611 (all coverage from this test)
fn main() -> () {
let x: u32 = 0_u32;
x = 1_u32 + 2_u32 + 3_u32;
println!(x);
}
Source location: tests/codegen.rs:628 (all coverage from this test)
fn main() -> () {
println!(identity::<S>(7_u32));
}
Source location: tests/codegen.rs:640 (all coverage from this test)
fn main() -> () { println!(left() + right()); }
}])
tc_ok()
ect_output("1\n2\n30\n")
)
}
#[test]
ion_in_call_arguments() {
alityTest::new(crates![crate test {
fn sum(x: i32, y: i32) -> i32 { return x + y; }
fn main() -> () {
println!(sum(1_i32 + 2_i32, sum(3_i32, 4_i32)));
}
Source location: tests/codegen.rs:653 (all coverage from this test)
fn main() -> () {
println!(sum(1_i32 + 2_i32, sum(3_i32, 4_i32)));
}
Source location: tests/codegen.rs:677 (all coverage from this test)
fn main() -> () {
let i_min: i128 = -170141183460469231731687303715884105728 _ i128;
let i_max: i128 = 170141183460469231731687303715884105727 _ i128;
let u_min: u128 = 0 _ u128;
let u_max: u128 = 340282366920938463463374607431768211455 _ u128;
println!(i_min);
println!(i_max);
println!(u_min);
println!(u_max);
}
Source location: tests/codegen.rs:693 (all coverage from this test)
fn main() -> () {
let s: S = S { b: second(), a: first() };
println!(s.a);
println!(s.b);
}
Source location: tests/codegen.rs:705 (all coverage from this test)
fn main() -> () {
println!(10_i32 - 3_i32);
}
Source location: tests/codegen.rs:721 (all coverage from this test)
fn main() -> () {
let w: Wrap<<S as Value>::Item> = Wrap::<<S as Value>::Item> { value: 7_u32 };
println!(w.value);
}
Source location: tests/codegen.rs:733 (all coverage from this test)
fn main() -> () {
println!(3_i32 - 10_i32);
}
Source location: tests/codegen.rs:745 (all coverage from this test)
fn main() -> () {
println!(10_i32 - 3_i32 - 2_i32);
}
Source location: tests/codegen.rs:757 (all coverage from this test)
fn main() -> () {
println!(10_i32 - 3_i32 + 2_i32);
}
Source location: tests/codegen.rs:769 (all coverage from this test)
fn main() -> () { println!(left() - right()); }
}])
tc_ok()
ect_output("1\n2\n7\n")
);
}
#[test]
er_subtraction_unsigned() {
alityTest::new(crates![crate Foo {
fn main() -> () {
println!(10_u32 - 3_u32);
}
Source location: tests/codegen.rs:781 (all coverage from this test)
fn main() -> () {
println!(10_u32 - 3_u32);
}
Source location: tests/codegen.rs:798 (all coverage from this test)
fn main() -> () {
let x: <S as Outer>::Item = 7_u32;
println!(x);
}
Source location: tests/codegen.rs:810 (all coverage from this test)
fn main() -> () {
println!(10_i32 - (3_i32 - 2_i32));
}
Source location: tests/codegen.rs:822 (all coverage from this test)
fn main() -> () {
println!(20_i32 - (10_i32 - (3_i32 - 1_i32)));
}
Source location: tests/codegen.rs:836 (all coverage from this test)
fn main() -> () {
let x: i32 = 10_i32;
(x = (x - 3_i32));
println!(x);
}
Source location: tests/codegen.rs:891 (all coverage from this test)
fn main() -> () {
println!(3_i32 * 4_i32);
}
Source location: tests/codegen.rs:905 (all coverage from this test)
fn main() -> () {
println!(2_i32 + 3_i32 * 4_i32);
println!(2_i32 * 3_i32 + 4_i32);
println!(2_i32 + 3_i32 * 4_i32 * 2_i32);
}
Source location: tests/codegen.rs:927 (all coverage from this test)
fn main() -> () {
println!(identity::<Number>(7_u32));
println!(identity::<Flag>(true));
println!(identity::<Number>(9_u32));
}
Source location: tests/codegen.rs:964 (all coverage from this test)
fn main() -> () {
let x: u32 = 1_u32;
exists<'a> {
let r: &'a mut u32 = &'a mut x;
x += update::<'a>(r);
}
println!(x);
}
Source location: tests/codegen.rs:976 (all coverage from this test)
fn main() -> () {
println!(-3_i32 * 4_i32);
}
Source location: tests/codegen.rs:988 (all coverage from this test)
fn main() -> () {
println!(3_u32 * 4_u32);
}
Source location: tests/codegen.rs:1000 (all coverage from this test)
fn main() -> () { println!(left() * right()); }
}])
tc_ok()
ect_output("1\n2\n12\n")
);
}
#[test]
plication_with_parentheses() {
alityTest::new(crates![crate Foo {
fn main() -> () {
println!((2_i32 + 3_i32) * 4_i32);
println!(2_i32 * (3_i32 + 4_i32));
}
Source location: tests/codegen.rs:1013 (all coverage from this test)
fn main() -> () {
println!((2_i32 + 3_i32) * 4_i32);
println!(2_i32 * (3_i32 + 4_i32));
}
Source location: tests/codegen.rs:1026 (all coverage from this test)
fn main() -> () {
println!(20_i32 - 2_i32 * 3_i32);
println!((20_i32 - 2_i32) * 3_i32);
}
Source location: tests/codegen.rs:1086 (all coverage from this test)
fn main() -> () {
let x: u32 = 1_u32;
x += 2_u32 + 3_u32;
println!(x);
}
Source location: tests/codegen.rs:1102 (all coverage from this test)
fn main() -> () {
let p: Pair = Pair { a: 1_u32, b: 10_u32 };
p.b += p.a;
println!(p.b);
}
Source location: tests/codegen.rs:1116 (all coverage from this test)
fn main() -> () {
let x: u32 = 20_u32;
x -= 2_u32 + 3_u32;
println!(x);
}
Source location: tests/codegen.rs:1132 (all coverage from this test)
fn main() -> () {
let p: Pair = Pair { a: 2_u32, b: 3_u32 };
p.b *= p.a + 4_u32;
println!(p.b);
println!(p.a);
}
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:27 (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:53 (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:100 (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:109 (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/consts.rs:131 (all coverage from this test)
#[test]
fn nested_const_bound_accepts_outer_parameter() {
FormalityTest::new(crates![crate Foo {
trait Foo<const C> where for<'a> type_of_const C is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:141 (all coverage from this test)
#[test]
fn nested_const_bound_accepts_inner_parameter() {
FormalityTest::new(crates![crate Foo {
#![feature(non_lifetime_binders)]
trait Foo where for<const C> type_of_const C is bool {}
}])
.skip_execute()
.ok()
}
Source location: tests/consts.rs:166 (all coverage from this test)
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:23 (all coverage from this test)
Source location: tests/drop.rs:43 (all coverage from this test)
Source location: tests/drop.rs:61 (all coverage from this test)
Source location: tests/drop.rs:108 (all coverage from this test)
Source location: tests/drop.rs:128 (all coverage from this test)
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)
fn multi_arg_ret<T, Y, U, I>(v0: T, v1: Y) -> (U, I) { trusted }
}])
p_execute()
tc_ok()
)
}
#[test]
ime() {
alityTest::new(crates![crate Foo {
// fn one_lt_arg<'a, T>(_: &'a T) -> () {}
fn one_lt_arg<'a, T>(v0: &'a T) -> ()
where
T: 'a, // FIXME(#202): Implied bounds should not have to be explicit
{ trusted }
}])
p_execute()
tc_ok()
)
}
#[test]
ed_return_type() {
alityTest::new(crates![
crate Foo {
fn simple_fn() { trusted }
fn one_arg<T>(v0: T) { trusted }
fn with_where<'a, T>(v0: &'a T)
where
T: 'a,
{ trusted }
}
Source location: tests/functions.rs:39 (all coverage from this test)
fn one_lt_arg<'a, T>(v0: &'a T) -> ()
where
T: 'a, // FIXME(#202): Implied bounds should not have to be explicit
{ trusted }
}])
p_execute()
tc_ok()
)
}
#[test]
ed_return_type() {
alityTest::new(crates![
crate Foo {
fn simple_fn() { trusted }
fn one_arg<T>(v0: T) { trusted }
fn with_where<'a, T>(v0: &'a T)
where
T: 'a,
{ trusted }
}
Source location: tests/functions.rs:55 (all coverage from this test)
Source location: tests/functions.rs:70 (all coverage from this test)
fn main() {
helper();
}
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:925 (all coverage from this test)
fn foo() -> bool {
let v1: bool = false;
return v1;
}
Source location: tests/mir_typeck.rs:949 (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:967 (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:987 (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:1014 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
break 'a;
}
return 0_u32;
}
Source location: tests/mir_typeck.rs:1073 (all coverage from this test)
fn foo() -> u32 {
'a: loop {
continue 'a;
}
return 0_u32;
}
Source location: tests/mir_typeck.rs:1142 (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:1168 (all coverage from this test)
fn foo() -> u32 {
'a: {
break 'a;
}
return 0_u32;
}
Source location: tests/mir_typeck.rs:1453 (all coverage from this test)
fn main() -> () { require_marker::<u32>; }
}])
tc_ok()
);
}
#[test]
fn_value_with_forwarded_trait_bound() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require<T>() -> () where T: Marker {}
fn outer<T>() -> () where T: Marker { require::<T>; }
fn main() -> () { outer::<u32>(); }
}])
tc_ok()
);
}
#[test]
bare_fn_value_with_satisfied_where_clause() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require() -> () where u32: Marker {}
fn main() -> () { require; }
}])
tc_ok()
);
}
#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}
#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
--> lib.rs
|
7 | pub fn outer<'a00, 'a01>() -> () {
| ---- ---- lifetime `'a01` defined here
| |
| lifetime `'a00` defined here
8 | require::<'a00, 'a01>;
| ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
|
= help: consider adding the following bound: `'a00: 'a01`
error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}
ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
let x: u32 = 1_u32;
x += 2_u8;
}
Source location: tests/mir_typeck.rs:1466 (all coverage from this test)
fn main() -> () { outer::<u32>(); }
}])
tc_ok()
);
}
#[test]
bare_fn_value_with_satisfied_where_clause() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require() -> () where u32: Marker {}
fn main() -> () { require; }
}])
tc_ok()
);
}
#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}
#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
--> lib.rs
|
7 | pub fn outer<'a00, 'a01>() -> () {
| ---- ---- lifetime `'a01` defined here
| |
| lifetime `'a00` defined here
8 | require::<'a00, 'a01>;
| ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
|
= help: consider adding the following bound: `'a00: 'a01`
error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}
ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
let x: u32 = 1_u32;
x += 2_u8;
}
Source location: tests/mir_typeck.rs:1478 (all coverage from this test)
fn main() -> () { require; }
}])
tc_ok()
);
}
#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}
#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
--> lib.rs
|
7 | pub fn outer<'a00, 'a01>() -> () {
| ---- ---- lifetime `'a01` defined here
| |
| lifetime `'a00` defined here
8 | require::<'a00, 'a01>;
| ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
|
= help: consider adding the following bound: `'a00: 'a01`
error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}
ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
let x: u32 = 1_u32;
x += 2_u8;
}
Source location: tests/mir_typeck.rs:1489 (all coverage from this test)
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}
#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
--> lib.rs
|
7 | pub fn outer<'a00, 'a01>() -> () {
| ---- ---- lifetime `'a01` defined here
| |
| lifetime `'a00` defined here
8 | require::<'a00, 'a01>;
| ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
|
= help: consider adding the following bound: `'a00: 'a01`
error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}
ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
let x: u32 = 1_u32;
x += 2_u8;
}
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/sized_trait.rs:14 (all coverage from this test)
fn main() -> () {}
}])
tc_ok()
)
}
: ADT Sized support is deferred; rustc accepts this empty struct.
test records the current limitation, not the intended Sized semantics.
#[test]
_bound_not_met_by_unimplemented_type() {
alityTest::new(crates![crate Foo {
struct S {}
trait Needs<T> where T: Sized {}
impl Needs<S> for u32 {}
}])
tc_ok()
(expect_test::expect![[r#"
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = &?lt_0 ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &?lt_0 ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = &?lt_0 mut ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: &?lt_0 mut ?ty_1, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [?lt_0, ?ty_1], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = (), via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: (), via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = bool, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: bool, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = i8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: i8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = isize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: isize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u128, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u16, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u32, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u64, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = u8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: u8, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: S = usize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: S, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
crates/formality-rust/src/prove/prove_normalize.rs:55:1: no applicable rules for prove_normalize_via { goal: usize, via: Sized(S), assumptions: {Sized(S)}, env: Env { variables: [], bias: Soundness, pending: [], allow_pending_outlives: false } }
the rule "trait implied bound" at (prove_predicate.rs) failed because
expression evaluated to an empty collection: `decls.trait_invariants()`
the rule "trait implied bound" at (prove_predicate.rs) failed because
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
}
#[test]
lue_trait_param_with_sized_bound_compiles_with_rustc() {
alityTest::new(crates![crate Foo {
fn consume<T>(value: T) -> () where T: Sized {}
trait Consumer<T> where T: Sized {
fn consume_value(value: T) -> () {}
}
Source location: tests/sized_trait.rs:142 (all coverage from this test)
Source location: tests/sized_trait.rs:153 (all coverage from this test)
Source location: tests/sized_trait.rs:164 (all coverage from this test)
Source location: tests/sized_trait.rs:175 (all coverage from this test)
Source location: tests/traits.rs:11 (all coverage from this test)
fn main() -> () { require_copy::<i128>(); }
}])
p_execute()
tc_ok()
);
}
#[test]
is_copy() {
alityTest::new(crates![crate test {
fn require_copy<T>() -> () where T: Copy { trusted }
fn main() -> () { require_copy::<u128>(); }
}])
p_execute()
tc_ok()
);
}
#[test]
_with_valid_fn() {
alityTest::new(crates![
crate core {
trait A {
fn a() -> ();
}
}
Source location: tests/traits.rs:22 (all coverage from this test)
fn main() -> () { require_copy::<u128>(); }
}])
p_execute()
tc_ok()
);
}
#[test]
_with_valid_fn() {
alityTest::new(crates![
crate core {
trait A {
fn a() -> ();
}
}
Source location: tests/traits.rs:36 (all coverage from this test)
Source location: tests/traits.rs:78 (all coverage from this test)
#[test]
fn associated_type_static_outlives_bound() {
FormalityTest::new(crates![crate Foo {
trait A { type Item: ['static]; }
}])
.skip_execute()
.rustc_ok()
.ok();
}
Source location: tests/traits.rs:88 (all coverage from this test)
#[test]
fn associated_type_outer_lifetime_outlives_bound() {
FormalityTest::new(crates![crate Foo {
trait A<'a> { type Item: ['a]; }
}])
.skip_execute()
.rustc_ok()
.ok();
}
Source location: tests/traits.rs:99 (all coverage from this test)
#[test]
fn associated_type_trait_and_outlives_bounds() {
FormalityTest::new(crates![crate Foo {
trait Bar {}
trait A<'a> { type Item: [Bar, 'a]; }
}])
.skip_execute()
.rustc_ok()
.ok();
}
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()
}