Update windows installer #1009
Milestone
Comments
celinval
pushed a commit
to celinval/rust-dev
that referenced
this issue
Jun 4, 2024
Deprecate kani::slice::any_slice in Kani 0.38.0 (and the related AnySlice struct), and remove it in a later version. Motivation: The Kani library's `slice::any_slice` API is doing more harm than benefit: it is meant to provide a convenient way for users to generate non-deterministic slices, but its current implementation aims to avoid any unsoundness by making sure that for the non-deterministic slice returned by the API, accessing memory beyond the slice length is flagged as an out-of-bounds access (see rust-lang#1009 for details). However, in practical scenarios, using it ends up causing memory to blowup for CBMC. Given that users may not care about this type of unsoundness, which is only possible through using a pointer dereference inside an unsafe block (see discussion in rust-lang#2634). Thus, we should leave it to the user to decide the suitable method for generating slices that fits their verification needs. For example, they can use Kani's alternative API, `any_slice_of_array` that extracts a slice of a non-deterministic start and end from a given array.
# for free
to join this conversation on GitHub.
Already have an account?
# to comment
No description provided.
The text was updated successfully, but these errors were encountered: