Negative coverage: borrow_check_expr_has_ty / block / premise borrow_check_expr(env, assumptions, state, expr, places_live_on_exit) => (ty_expr, state)
Premise at line 363. Observed failure causes: failed_judgment.
block| Line | Coverage | Source |
|---|---|---|
| 363 | 36 | (borrow_check_expr(env, assumptions, state, expr, places_live_on_exit) => (ty_expr, state)) |
| 364 | 7 | (prove_assignable(env, assumptions, state, ty_expr, ty) => state) |
| ──────── ("block") | ||
| 366 | 118 | (borrow_check_expr_has_ty(env, assumptions, state, expr, ty, places_live_on_exit) => state) |
36 tests failed proving this premise:
Source location: src/test_util.rs:464 (all coverage from this test)
#[test]
fn borrowck_err_checks_rustc_err_once() {
let before = rustc_runs();
FormalityTest::new(MOVED)
.rustc_err(expect_test::expect![[r#"
error[E0382]: use of moved value: `x`
--> lib.rs
|
6 | let mut x: Datum = Datum { value: 0_u32 };
| ----- move occurs because `x` has type `Datum`, which does not implement the `Copy` trait
7 | let mut y: Datum = x;
| - value moved here
8 | let mut z: Datum = x;
| ^ value used here after move
|
note: if `Datum` implemented `Clone`, you could clone the value
--> lib.rs
|
1 | pub struct Datum {
| ^^^^^^^^^^^^^^^^ consider implementing `Clone` for this type
...
7 | let mut y: Datum = x;
| - you could clone this value
For more information about this error, try `rustc --explain E0382`.
error: could not compile `Foo` (lib) due to 1 previous error
"#]])
.borrowck_err(BorrowCheckFailure::All, expect_test::expect![[r#"
the rule "access_permitted" at (nll.rs) failed because
condition evaluated to false: `match access.kind
{
AccessKind::Write =>
check_place_writable(&state, &access.place.to_place_expression()),
AccessKind::Read | AccessKind::Move =>
check_place_initialized(&state, &access.place.to_place_expression()),
}`"#]]);
assert_eq!(rustc_runs() - before, 1);
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
Source location: src/test_util.rs:479 (all coverage from this test)
#[test]
#[should_panic(expected = "expected `rustc` to succeed but it failed")]
fn borrowck_err_enforces_rustc_ok() {
FormalityTest::new(MOVED).rustc_ok().borrowck_err(
BorrowCheckFailure::All,
expect_test::expect![[r#"
the rule "access_permitted" at (nll.rs) failed because
condition evaluated to false: `match access.kind
{
AccessKind::Write =>
check_place_writable(&state, &access.place.to_place_expression()),
AccessKind::Read | AccessKind::Move =>
check_place_initialized(&state, &access.place.to_place_expression()),
}`"#]],
);
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
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);
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "exists"nll.rs:330borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "if"nll.rs:223borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350rule "block"nll.rs:363borrow_check_expr failednll.rs:371rule "ref"nll.rs:521access_permitted failednll.rs:862rule "access_permitted"nll.rs:878access_permitted_by_loans failednll.rs:885rule "access_permitted_by_loans"nll.rs:898access_permitted_by_loan failednll.rs:905args
rule "borrow of disjoint places"nll.rs:920 (failed: if_false)rule "loan is dead"nll.rs:967loan_not_required_by_live_places failednll.rs:1296rule "loan_not_required_by_live_places"nll.rs:1321loan_not_required_by_live_place failednll.rs:1328args
rule "loan is not required by type"nll.rs:1348loan_not_required_by_parameter failednll.rs:1396args
rule "rigid-ty"nll.rs:1416loan_not_required_by_parameters failednll.rs:1533args
rule "loan_not_required_by_parameters"nll.rs:1554loan_not_required_by_parameter failednll.rs:1396args
rule "lifetime"nll.rs:1506loan_cannot_outlive failednll.rs:1513args
rule "loan_cannot_outlive"nll.rs:1526 (failed: if_false)
rule "universal-variable"nll.rs:1490loan_cannot_outlive_universal_regions failednll.rs:1240args
rule "loan_not_required_by_universal_regions"nll.rs:1267 (failed: if_false)
rule "write-indirect"nll.rs:947 (failed: if_let)rule "write-indirect"nll.rs:949 (failed: if_false)
Source location: tests/borrowck.rs:172 (all coverage from this test)
fn foo() -> Datum {
let x: Datum = Datum { value: 0_u32 };
let y: Datum = x;
let z: Datum = x;
return z;
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
Source location: tests/borrowck.rs:393 (all coverage from this test)
fn foo() -> Datum {
let x: Datum = Datum { value: 0_u32 };
if true {
let y: Datum = x;
}
let z: Datum = x;
return z;
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
Source location: tests/borrowck.rs:532 (all coverage from this test)
fn foo() -> u32 {
let x: Pair = Pair {
first: Datum { value: 1_u32 },
second: Datum { value: 2_u32 },
};
let a: Datum = x.first;
let b: Pair = x;
return 0_u32;
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
Source location: tests/borrowck.rs:580 (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.first;
return b;
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
Source location: tests/borrowck.rs:628 (all coverage from this test)
fn foo() -> Datum {
let x: Pair = Pair {
first: Datum { value: 1_u32 },
second: Datum { value: 2_u32 },
};
let a: Pair = x;
let b: Datum = x.first;
return b;
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
Source location: tests/borrowck.rs:672 (all coverage from this test)
fn foo() -> u32 {
let x: Outer = Outer {
foo: Inner { bar: 1_u32 },
};
let a: Inner = x.foo;
let b: u32 = x.foo.bar;
return b;
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
rule "place"nll.rs:547access_permitted failednll.rs:862args
rule "access_permitted"nll.rs:874 (failed: if_false)
Source location: tests/borrowck.rs:721 (all coverage from this test)
fn foo() -> Datum {
exists<'r0, 'r1> {
let x: Datum = Datum { value: 0_u32 };
let r: &'r0 Datum = &'r1 x;
let y: Datum = *r;
return y;
}
}
Failed proof tree
check_all_crates failedmod.rs:42args
rule "check all prefixes"mod.rs:54check_crate failedmod.rs:61args
rule "check crate"mod.rs:74check_crate_item failedmod.rs:179rule "free fn"mod.rs:207check_free_fn failedfns.rs:14args
rule "check free fn"fns.rs:24check_fn failedfns.rs:31args
rule "check fn"fns.rs:54check_fn_body failedfns.rs:61args
rule "expr fn body"fns.rs:89borrow_check failednll.rs:124args
rule "borrow_check"nll.rs:135borrow_check_block failednll.rs:142rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "exists"nll.rs:302borrow_check_block failednll.rs:142args
rule "basic block"nll.rs:157borrow_check_statement failednll.rs:174args
rule "let"nll.rs:189borrow_check_expr_has_ty failednll.rs:350args
rule "block"nll.rs:363borrow_check_expr failednll.rs:371args
rule "place"nll.rs:549prove_place_is_movable failednll.rs:1040args
rule "copy"nll.rs:1078prove_ty_is_copy failednll.rs:1021rule "trait"nll.rs:1033prove failedfunction.rs:250args
rulefunction.rs:250prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "positive impl"prove_predicate.rs:71prove failedprove_predicate.rs:71args
ruleprove_predicate.rs:71prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:69prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-l"prove_eq.rs:69prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "positive impl"prove_predicate.rs:71prove failedprove_predicate.rs:71args
ruleprove_predicate.rs:71prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:69prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "symmetric"prove_eq.rs:38prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-l"prove_eq.rs:69prove_after failedprove_after.rs:8args
rule "prove_after"prove_after.rs:19prove failedprove_after.rs:19args
ruleprove_after.rs:19prove_predicate_list failedprove_predicate_list.rs:8args
rule "some"prove_predicate_list.rs:26prove_predicate failedprove_predicate.rs:22args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "assumption"prove_predicate.rs:48prove_via failedprove_via.rs:9args
rule "eq"prove_predicate.rs:115prove_eq failedprove_eq.rs:23args
rule "normalize-l"prove_eq.rs:68prove_normalize failedprove_normalize.rs:22args
rule "normalize-via-assumption"prove_normalize.rs:36prove_normalize_via failedprove_normalize.rs:55args
rule "normalize-via-assumption"prove_normalize.rs:36
Source location: tests/borrowck.rs:1476 (all coverage from this test)
fn foo() -> Datum {
exists<'r0, 'r1> {
let x: Datum = Datum { value: 0_u32 };
let r: &'r0 mut Datum = &'r1 mut x;
let y: Datum = *r;
return y;
}
}
Proof trees omitted for the remaining 26 tests; each one is on its test’s page in Coverage by test.
Source location: tests/borrowck.rs:2232 (all coverage from this test)
fn foo() -> Datum {
exists<'r0, 'r1> {
let x: Datum = Datum { value: 0_u32 };
let r: &'r0 Datum = &'r1 x;
let y: Datum = x;
return *r;
}
}
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: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:3470 (all coverage from this test)
fn foo<'a, 'b>(a: &'a u32) -> &'b u32 {
let r: &'b u32 = identity::<&'b u32>(a);
return r;
}
Source location: tests/borrowck.rs:3536 (all coverage from this test)
fn bar() -> u32 {
exists<'r0, 'r1, 'r2> {
let v: u32 = 0_u32;
let p: &'r0 u32 = &'r1 v;
let _: u32 = foo::<'r2>(&'r2 mut v);
return *p;
}
}
Source location: tests/borrowck.rs:3618 (all coverage from this test)
fn foo() -> u32 {
exists<'r0, 'r1> {
let v1: u32 = 22_u32;
let v2: &'r0 mut u32 = &'r1 mut v1;
let w: Wrapper = Wrapper { value: v1 };
return *v2;
}
}
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:3891 (all coverage from this test)
fn foo(f: Pair) -> () {
let s: Datum = f.x;
}
Source location: tests/borrowck.rs:4035 (all coverage from this test)
fn foo<'a, 'b>(p: &'a mut u32) -> u32 {
let q: &'b mut u32 = &'b mut *p;
q;
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: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/mir_typeck.rs:345 (all coverage from this test)
fn bar() -> u32 {
let v1: u32 = foo(0_u32);
return v1;
}
Source location: tests/mir_typeck.rs:392 (all coverage from this test)
fn bar(v1: ()) -> () {
let v0: () = foo(v1);
return v0;
}
Source location: tests/mir_typeck.rs:416 (all coverage from this test)
fn bar(v1: u32) -> u32 {
let v0: u32 = identity(v1);
return v0;
}
Source location: tests/mir_typeck.rs:488 (all coverage from this test)
fn bar(v1: u32) -> u32 {
let v0: u32 = identity::<bool>(v1);
return v0;
}
Source location: tests/mir_typeck.rs:532 (all coverage from this test)
fn bar(v1: u32) -> u32 {
let v0: u32 = identity::<u32>(v1, v1);
return v0;
}
Source location: tests/mir_typeck.rs:568 (all coverage from this test)
fn bar(v1: u32) -> u32 {
let v0: u32 = identity::<u32, u32>(v1);
return v0;
}
Source location: tests/mir_typeck.rs:848 (all coverage from this test)
fn foo (v1: u32) -> u32 {
let v2: Dummy = Dummy { value: false };
return v1;
}
Source location: tests/mir_typeck.rs:876 (all coverage from this test)
fn foo (v1: u32) -> u32 {
let v2: u32 = Nonexistent { value: false };
return v1;
}
Source location: tests/mir_typeck.rs:902 (all coverage from this test)
fn main() -> () {
let s: S = S { x: 1_u32, x: 2_u32 };
}
Source location: tests/mir_typeck.rs:1218 (all coverage from this test)
fn foo() -> () {
let x: i32 = 1_i32 + 2_u32;
}
Source location: tests/mir_typeck.rs:1270 (all coverage from this test)
fn foo() -> () {
let x: i32 = 10_i32 - 3_u32;
}
Source location: tests/mir_typeck.rs:1323 (all coverage from this test)
fn foo() -> () {
let x: i32 = 3_i32 * 4_u32;
}
Source location: tests/mir_typeck.rs:1349 (all coverage from this test)
fn foo() -> () {
let x: bool = true * false;
}