flux_core/slice/
index.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
#[cfg(flux)]
use core::ops;

use flux_attrs::*;

#[extern_spec(core::slice)]
impl<T, I: SliceIndex<[T]>> ops::Index<I> for [T] {
    #![reft(
        fn in_bounds(len: int, idx: I) -> bool {
            <I as SliceIndex<[T]>>::in_bounds(idx, len)
        }
    )]

    #[sig(fn(&Self[@len], {I[@idx] | <Self as ops::Index<I>>::in_bounds(len, idx)}) -> &I::Output)]
    fn index(&self, index: I) -> &I::Output;
}

#[extern_spec(core::slice)]
trait SliceIndex<T> {
    #![reft(fn in_bounds(idx: Self, v: T) -> bool { true })] //
}

#[extern_spec(core::slice)]
impl<T> SliceIndex<[T]> for usize {
    #![reft(fn in_bounds(idx: int, len: int) -> bool { idx < len })] //
}

#[extern_spec(core::slice)]
impl<T> SliceIndex<[T]> for ops::Range<usize> {
    #![reft(
        fn in_bounds(r: ops::Range<int>, len: int) -> bool {
            r.start <= r.end && r.end < len
        }
    )] //
}

#[cfg(flux_sysroot_test)]
mod tests {
    #![allow(dead_code)]

    use flux_attrs::*;

    #[sig(fn(&[i32]{n: n > 10}))]
    fn test00(xs: &[i32]) {
        let _y = &xs[0..1];
    }

    #[should_fail]
    fn test01(xs: &[i32]) {
        let _y = &xs[0..1];
    }
}