flux_core/slice/
index.rs

1#[cfg(flux)]
2use core::ops;
3
4use flux_attrs::*;
5
6#[extern_spec(core::slice)]
7impl<T, I: SliceIndex<[T]>> ops::Index<I> for [T] {
8    #![reft(
9        fn in_bounds(len: int, idx: I) -> bool {
10            <I as SliceIndex<[T]>>::in_bounds(idx, len)
11        }
12    )]
13
14    #[sig(fn(&Self[@len], {I[@idx] | <Self as ops::Index<I>>::in_bounds(len, idx)}) -> &I::Output)]
15    fn index(&self, index: I) -> &I::Output;
16}
17
18#[extern_spec(core::slice)]
19trait SliceIndex<T> {
20    #![reft(fn in_bounds(idx: Self, v: T) -> bool { true })] //
21}
22
23#[extern_spec(core::slice)]
24impl<T> SliceIndex<[T]> for usize {
25    #![reft(fn in_bounds(idx: int, len: int) -> bool { idx < len })] //
26}
27
28#[extern_spec(core::slice)]
29impl<T> SliceIndex<[T]> for ops::Range<usize> {
30    #![reft(
31        fn in_bounds(r: ops::Range<int>, len: int) -> bool {
32            r.start <= r.end && r.end < len
33        }
34    )] //
35}
36
37#[cfg(flux_sysroot_test)]
38mod tests {
39    #![allow(dead_code)]
40
41    use flux_attrs::*;
42
43    #[sig(fn(&[i32]{n: n > 10}))]
44    fn test00(xs: &[i32]) {
45        let _y = &xs[0..1];
46    }
47
48    #[should_fail]
49    fn test01(xs: &[i32]) {
50        let _y = &xs[0..1];
51    }
52}
flux_core/slice/index.rs

flux_core/slice/
index.rs
