Closed enjhnsn2 closed 9 months ago
This is a known limitation. Constants have to be explicitly marked so they can be used inside refinements like so:
#[flux::constant]
pub const EIGHT: i32 = 8;
#[flux::sig(fn() -> i32{r: r == EIGHT})]
fn test() -> i32 {
8
}
The annotation will make the constant globally available no matter where it was defined.
The underlying issue is that there's no easy way to resolve names into rust items. The compiler doesn't offer an API for this. So we need to reimplement name resolution or find a good enough hack.
Noted, I was not aware of the #[flux::constant]
API. I will close the issue
This code verifies correctly:
but this code fails:
with the error: