Refining struct with no invariants causes `assignment might be unsafe` error #755

enjhnsn2 · 2024-08-26T18:40:00Z

Hello, when I verify the following code implementing a SubSlice data structure:

pub struct FluxRange {
    pub start: usize,
    pub end: usize,
}

pub struct SubSlice<'a, T> {
    internal: &'a [T],
    active_range: FluxRange,
}

impl<'a, T> SubSlice<'a, T> {
    pub fn reset(&mut self) {
        self.active_range = FluxRange{ start: 0, end: self.internal.len()};
    }
}

it passes.

However, when I try to add indexes to this data structure:

#[flux_rs::refined_by(start: int, end: int)]
pub struct FluxRange {
    #[field(usize[start])]
    pub start: usize,
    #[field(usize[end])]
    pub end: usize,
}

#[flux_rs::refined_by(lo: int, hi: int, len: int)]
pub struct SubSlice<'a, T> {
    #[field(&[T][len])]
    internal: &'a [T],
    #[field(FluxRange[lo, hi])]
    active_range: FluxRange,
}

impl<'a, T> SubSlice<'a, T> {
    pub fn reset(&mut self) {
        self.active_range = FluxRange{ start: 0, end: self.internal.len()};
    }
}

it fails with:

error[E0999]: assignment might be unsafe
   --> src/main.rs:251:9
    |
251 |         self.active_range = FluxRange{ start: 0, end: self.internal.len()};
    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This is a bit confusing to me, as I would assume that if you add indexes to a struct, it should behave the same until you try to state invariants about it (e.g. lo < hi && hi < len). By adding indexes to the fields, did I assert something about the struct's behavior?

The text was updated successfully, but these errors were encountered:

nilehmann added the mut-ref-unfolding Related to unfolding of mutable references label Aug 27, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refining struct with no invariants causes `assignment might be unsafe` error #755

Refining struct with no invariants causes `assignment might be unsafe` error #755

Refining struct with no invariants causes assignment might be unsafe error #755

Refining struct with no invariants causes assignment might be unsafe error #755

Comments

Refining struct with no invariants causes `assignment might be unsafe` error #755

Refining struct with no invariants causes `assignment might be unsafe` error #755