flux-rs / flux

Refinement Types for Rust
MIT License
632 stars 17 forks source link

Hex integer literals in refined function signature crash verification #573

Closed enjhnsn2 closed 8 months ago

enjhnsn2 commented 9 months ago

This code verifies:

#[flux::sig(fn() -> i32{r: r == 8})]
fn test() -> i32 {
    8
}

But this code fails:

#[flux::sig(fn() -> i32{r: r == 0x8})]
fn test() -> i32 {
    8
}

with the error:

error[FLUX]: integer literal is too large
 --> src/lib.rs:3:33
  |
3 | #[flux::sig(fn() -> i32{r: r == 0x8})]
  |                                 ^^^

error: aborting due to previous error
nilehmann commented 9 months ago

The relevant code is here https://github.com/flux-rs/flux/blob/main/crates/flux-desugar/src/desugar.rs/#L1097-L1099

We try to parse the literal into an integer without considering it can be in hexadecimal.

enjhnsn2 commented 9 months ago

ok, I'll take a look today and see if I can fix it