search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.08k stars 58 forks source link

About repeat expression in array #1123

Closed zpzigi754 closed 1 month ago

zpzigi754 commented 1 month ago

I've tested with the below example.

#![allow(unused_imports)]
use vstd::prelude::*;

verus! {

fn main() {
    let array: [i32; 3] = [0; 3];
    // XXX: if the below is used, it would work
    //let array: [i32; 3] = [0, 0, 0];
}

} // verus!

It says that The verifier does not yet support the following Rust feature: repeat expressions. I think that supporting the repeat expression in array initialization would be helpful for the users if the size of the target array to verify is big.

Is there any alternative way of creating a large array without the repeat expression in verus? I also wonder what is the main obstacle of supporting the repeat expression in verus.

utaal commented 1 month ago

Hi @zpzigi754, thanks for the report, and for trying out Verus! I don't think we currently have a workaround for this, (@tjhance ?). Anyway, while this is indeed important, it's a feature request -- so I'll convert it to a discussion.