| 12345678910111213141516171819202122232425 |
- .. SPDX-License-Identifier: GPL-2.0 or GPL-3.0
- .. Copyright © 2019 Ariadne Devos
- .. index::
- single: slice
- Slices: positive-length array ranges
- ====================================
- Slices point to a region in memory, of a certain length.
- s² took the concept from Rust [#frustslice]_. Due to
- Spectre mitigation issues, slices typically must be
- positive in length.
- A slice is specified as SliceCap<impl T>(c: T& -> Cap, length:
- nat, p: T \*), where `c` indicates the capability.
- SliceCap<impl T>(c: T& -> Cap, length: nat, p: T *) :=
- 0 <= length <= SIZE_MAX,
- ∀{i | 0 <= i < length} (c . (index a))
- .. rubric:: footnotes
- XXX Rust reference
|
