search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.25k stars 72 forks source link

`external_body` consts panic the verifier #1322

Open matthias-brun opened 4 weeks ago

matthias-brun commented 4 weeks ago

[edited by @utaal]

use vstd::prelude::verus; verus!{

#[verifier(external_body)]
const A: usize ensures 32 <= A <= 52 { unimplemented!() }

}

panics verus.