Traits§
Functions§
- Allocated
- Formal:
Allocated(p, T, len, A): ∀ i ∈ 0..sizeof(T)*len, allocator(p+i) = A - Deref
- Formal:
Deref(p, T, len) = Allocated(p, T, len, *) && InBound(p, T, len) - InBound
- Formal:
InBound(p, T, len): mem(p, p+ sizeof(T) * len) ∈ single allocated object - Size
- Formal:
sizeof(T) = c, c ∈ {num, unknown, any} - Valid
Ptr - Official ptr safety doc: https://doc.rust-lang.org/std/ptr/index.html#safety.