search

AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
21 stars 1 forks source link

subtype mismatch in black_box #37

Open franziskuskiefer opened 2 months ago

franziskuskiefer commented 2 months ago

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] -> ())