Signature:
prove_wf(_decls: Program, env: Env, assumptions: Wcs, goal: 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.
universal variables
| Line | Coverage | Source |
|---|
| | ──────── ("universal variables") |
| 31 | 107 | (prove_wf(_decls, env, _assumptions, UniversalVar { .. }) => Constraints::none(env)) |
references
| Line | Coverage | Source |
|---|
| 36 | ✗ | (let (lt, ty) = parameters.downcast_err::<(Lt, Ty)>()?) |
| 37 | 1 | (prove_wf_recursive(decls, env, assumptions, ty) => c) |
| 38 | ✗ | (prove_after(decls, c, assumptions, Relation::outlives(ty, lt)) => c) |
| | ──────── ("references") |
| 40 | 27 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Ref(_), parameters }) => c) |
raw-pointers
| Line | Coverage | Source |
|---|
| 45 | ✗ | (let (ty,) = parameters.downcast_err::<(Ty,)>()?) |
| 46 | ✗ | (prove_wf_recursive(decls, env, assumptions, ty) => c) |
| | ──────── ("raw-pointers") |
| 48 | ✗ | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Raw(_), parameters }) => c) |
tuples
| Line | Coverage | Source |
|---|
| 52 | ✗ | (for_all(decls, env, assumptions, parameters, &prove_wf_recursive) => c) |
| | ──────── ("tuples") |
| 54 | 36 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Tuple(_), parameters }) => c) |
integers and booleans
| Line | Coverage | Source |
|---|
| 58 | ✗ | (for_all(decls, env, assumptions, parameters, &prove_wf_recursive) => c) |
| | ──────── ("integers and booleans") |
| 60 | 81 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c) |
ADT
| Line | Coverage | Source |
|---|
| 64 | ✗ | (for_all(decls, env, assumptions, parameters, &prove_wf_recursive) => c) |
| 65 | ✗ | (let t = decls.program().adt_item_named(adt_id)?.to_adt()) |
| 66 | N/A | (let t = t.binder.instantiate_with(parameters).unwrap()) |
| 67 | 4 | (prove_after(decls, c, assumptions, &t.where_clauses) => c) |
| | ──────── ("ADT") |
| 69 | 20 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c) |
static lifetime
| Line | Coverage | Source |
|---|
| | ──────── ("static lifetime") |
| 74 | 1 | (prove_wf(_decls, env, _assumptions, LtData::Static) => Constraints::none(env)) |
scalar constants are always wf
| Line | Coverage | Source |
|---|
| | ──────── ("scalar constants are always wf") |
| 79 | 3 | (prove_wf(_decls, env, _assumptions, ConstData::Scalar(_)) => Constraints::none(env)) |
aliases
| Line | Coverage | Source |
|---|
| 83 | ✗ | (prove_alias_wf(decls, env, assumptions, name, parameters) => c) |
| | ──────── ("aliases") |
| 85 | 1 | (prove_wf(decls, env, assumptions, AliasTy { name, parameters }) => c) |