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

Mutable slices with ranges #14

Open franziskuskiefer opened 4 months ago

franziskuskiefer commented 4 months ago

Eurydice fails when trying to extract something like fun(&mut buf[0..8]).

See for example this change https://github.com/cryspen/libcrux/commit/a84d517beea0b7917385b41367e495c869549496#diff-cac793f2bb8c1229c9c3bbd71a681b9daf1cecd9646ed3e2a5ab208f47c9fc48R38

msprotz commented 4 months ago

Looking at the commit the issue appears to be with [..] specifically, correct?

franziskuskiefer commented 4 months ago

Full range is definitely an issue. But I think I the others, like [0..8] failed as well. But only when mutable. We should do small reproducers for these.