kani

Module slice

Source

Functionsยง

  • any_slice_of_array
    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.
  • any_slice_of_array_mut
    A mutable version of the previous function