Module kani::slice

source ·


  • Given an array arr of length LENGTH, this function returns a valid slice of arr with non-deterministic start and end points. This is useful in situations where one wants to verify that all possible slices of a given array satisfy some property.
  • A mutable version of the previous function