Negative coverage: borrow_check_expr / call / premise if input_tys.len() == args.len()
Premise at line 408. Observed failure causes: if_false.
call| Line | Coverage | Source |
|---|---|---|
| 388 | 3 | (borrow_check_expr( env, assumptions, state, callee, args.live_before(env, &state, places_live), ) => (callee_ty, state)) |
| 397 | ✗ | (prove_ty_is_rigid(env, assumptions, state, callee_ty) => (RigidTy { name: RigidName::FnDef(fn_id), parameters }, state)) |
| 400 | ✗ | (let Fn { id: _, safety, binder } = env.crates().fn_named(fn_id)?) |
| 402 | ✗ | (ProvenSet::singleton((safety, ProofTree::leaf("safety"))) => Safety::Safe) |
| 403 | ✗ | (let FnBoundData { input_args, output_ty, where_clauses, body: _ } = binder.instantiate_with(parameters)?) |
| 407 | N/A | (let input_tys: Vec<Ty> = input_args.iter().map(|a| a.ty.clone()).collect()) |
| 408 | 1 | (if input_tys.len() == args.len()) |
| 410 | ✗ | (for_all(i in 0..args.len()) with(state) (borrow_check_expr_has_ty(env, assumptions, state, &args[i], &input_tys[i], places_live) => state)) |
| 413 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| ──────── ("call") | ||
| 415 | 14 | (borrow_check_expr(env, assumptions, state, Expr::Call { callee, args }, places_live) => (output_ty, state)) |
1 test failed proving this premise:
Source location: tests/mir_typeck.rs:383
fn bar(v1: u32) -> u32 {
let v0: u32 = identity::<u32>(v1, v1);
return v0;
}
Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "free fn"mod.rs:191check_free_fn failedfns.rs:14rule "check free fn"fns.rs:24check_fn failedfns.rs:31rule "check fn"fns.rs:55check_fn_body failedfns.rs:62rule "expr fn body"fns.rs:90borrow_check failednll.rs:126rule "borrow_check"nll.rs:137borrow_check_block failednll.rs:144rule "basic block"nll.rs:159borrow_check_statement failednll.rs:176rule "let"nll.rs:193borrow_check_expr_has_ty failednll.rs:319rule "block"nll.rs:332borrow_check_expr failednll.rs:340rule "call"nll.rs:408 (failed: if_false)