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") |
| 28 | 141 | (prove_wf(_decls, env, _assumptions, UniversalVar { .. }) => Constraints::none(env)) |
references
| Line | Coverage | Source |
|---|
| 33 | ✗ | (let (lt, ty) = parameters.downcast_err::<(Lt, Ty)>()?) |
| 34 | 1 | (prove_wf_recursive(decls, env, assumptions, ty) => c) |
| 35 | ✗ | (prove_after(decls, c, assumptions, Relation::outlives(ty, lt)) => c) |
| | ──────── ("references") |
| 37 | 59 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Ref(_), parameters }) => c) |
raw-pointers
| Line | Coverage | Source |
|---|
| 42 | ✗ | (let (ty,) = parameters.downcast_err::<(Ty,)>()?) |
| 43 | ✗ | (prove_wf_recursive(decls, env, assumptions, ty) => c) |
| | ──────── ("raw-pointers") |
| 45 | ✗ | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Raw(_), parameters }) => c) |
tuples
| Line | Coverage | Source |
|---|
| 49 | ✗ | (for_all(decls, env, assumptions, parameters, &prove_wf_recursive) => c) |
| | ──────── ("tuples") |
| 51 | 36 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Tuple(_), parameters }) => c) |
integers and booleans
| Line | Coverage | Source |
|---|
| 55 | ✗ | (for_all(decls, env, assumptions, parameters, &prove_wf_recursive) => c) |
| | ──────── ("integers and booleans") |
| 57 | 112 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c) |
ADT
| Line | Coverage | Source |
|---|
| 61 | ✗ | (for_all(decls, env, assumptions, parameters, &prove_wf_recursive) => c) |
| 62 | ✗ | (let t = decls.program().adt_item_named(adt_id)?.to_adt()) |
| 63 | N/A | (let t = t.binder.instantiate_with(parameters).unwrap()) |
| 64 | 4 | (prove_after(decls, c, assumptions, &t.where_clauses) => c) |
| | ──────── ("ADT") |
| 66 | 50 | (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c) |
static lifetime
| Line | Coverage | Source |
|---|
| | ──────── ("static lifetime") |
| 71 | 1 | (prove_wf(_decls, env, _assumptions, LtData::Static) => Constraints::none(env)) |
scalar constants are always wf
| Line | Coverage | Source |
|---|
| | ──────── ("scalar constants are always wf") |
| 76 | 3 | (prove_wf(_decls, env, _assumptions, ConstData::Scalar(_)) => Constraints::none(env)) |
aliases
| Line | Coverage | Source |
|---|
| 80 | ✗ | (prove_alias_wf(decls, env, assumptions, name, parameters) => c) |
| | ──────── ("aliases") |
| 82 | 1 | (prove_wf(decls, env, assumptions, AliasTy { name, parameters }) => c) |