AeneasVerif/eurydice

subtype mismatch in black_box

franziskuskiefer opened this issue · 1 comments

The following code

fn b(x: &[u8]) -> [u8; 32] {
    [0u8; 32]
}

pub fn bb(x: &[u8]) -> [u8; 32] {
    core::hint::black_box(b(x))
}

produces the following error when running it through eurydice

subtype mismatch:
  uint8_t[32size_t] -> uint8_t[32size_t] (a.k.a. uint8_t[32size_t] -> uint8_t[32size_t]) vs:
  uint8_t[32size_t] -> uint8_t[32size_t] -> () (a.k.a. uint8_t[32size_t] -> uint8_t[32size_t] -> ())