Signature:
main() { /// let mut i = 22; /// let p: &'?0 i32 = &i; /// let q: &'?1 i32 = p; // subtyping requires `&'?0 i32 <: &'?1: i32` requires `'?0: '?1` /// if condition() { /// i += 1; // <- ok, `p` is dead /// } else { /// i += 1; // <- error, `p` is live (via `q`) /// println("{q}"); /// } /// } /// ``` pub fn prove_outlives( _decls: Program, env: Env, assumptions: Wcs, a: Parameter, b: Parameter,) => Constraints
The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.
static outlives everything
| Line | Coverage | Source |
|---|
| | ──────── ("static outlives everything") |
| 52 | ✗ | (prove_outlives(_decls, _env, _assumptions, LtData::Static, _b) => Constraints::none(env)) |
anything outlives erased
| Line | Coverage | Source |
|---|
| | ──────── ("anything outlives erased") |
| 58 | ✗ | (prove_outlives(_decls, _env, _assumptions, _a, LtData::Erased) => Constraints::none(env)) |
erased outlives static
| Line | Coverage | Source |
|---|
| | ──────── ("erased outlives static") |
| 64 | ✗ | (prove_outlives(_decls, _env, _assumptions, LtData::Erased, LtData::Static) => Constraints::none(env)) |
rigid types
| Line | Coverage | Source |
|---|
| 69 | ✗ | (prove(decls, env, assumptions, Wcs::all_outlives(parameters, b)) => c) |
| | ──────── ("rigid types") |
| 71 | ✗ | (prove_outlives(decls, env, assumptions, RigidTy { name: _, parameters }, b) => c) |
outlive through assumption
| Line | Coverage | Source |
|---|
| 77 | N/A | (let all_outlives = transitively_outlived_by(assumptions, a)) |
| 78 | ✗ | (if all_outlives.contains(&*b)) |
| | ──────── ("outlive through assumption") |
| 80 | ✗ | (prove_outlives(_decls, env, assumptions, a, b) => Constraints::none(env)) |
anything can be pending
| Line | Coverage | Source |
|---|
| 87 | ✗ | (if env.allow_pending_outlives()) |
| | ──────── ("anything can be pending") |
| 89 | ✗ | (prove_outlives(_decls, env, _assumptions, a, b) => Constraints::none(
env.with_pending(Relation::outlives(a, b))
)) |