judgment_fn! {
/// A *outlives* B if --
///
/// * "as long as B is valid, A is valid"
/// * "if A is invalidated, B *may* be invalidated"
///
/// Outlives is "reflexive" -- `'a: 'a`.
///
/// Examples:
///
/// * `'static: 'a` -- true
/// *
///
/// Borrow check flow example
///
/// ```rust,ignore
/// fn 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: Predicates,
a: Parameter,
b: Parameter,
) => Constraints {
/* rules omitted */
}
}
Source: crates/formality-rust/src/prove/prove_outlives.rs:8
No applicable rule observed: at least one test exercised this judgment with no matching rule.
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, Lt::Static, _b) => Constraints::none(env)) |
anything outlives erased
| Line | Coverage | Source |
|---|
| | ──────── ("anything outlives erased") |
| 58 | ✗ | (prove_outlives(_decls, _env, _assumptions, _a, Lt::Erased) => Constraints::none(env)) |
erased outlives static
| Line | Coverage | Source |
|---|
| | ──────── ("erased outlives static") |
| 64 | ✗ | (prove_outlives(_decls, _env, _assumptions, Lt::Erased, Lt::Static) => Constraints::none(env)) |
rigid types
| Line | Coverage | Source |
|---|
| 69 | ✗ | (prove(decls, env, assumptions, Predicates::all_outlives(parameters, b)) => c) |
| | ──────── ("rigid types") |
| 71 | 55 | (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 | 195 | (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 | 29 | (prove_outlives(_decls, env, _assumptions, a, b) => Constraints::none(
env.with_pending(AtomicPredicate::outlives(a, b))
)) |
How to read this page