Nadrieril
Nadrieril
I see, thanks for the Kani link. Compared to Kani at the time [this](https://model-checking.github.io/kani/rfc/rfcs/0001-mir-linker.html) was written, we already do the reachability analysis, but we have the same issue of only...
Actually before thinking of shipping that ourselves, you may be able to get what you want by rebuilding the stdlib yourselves with `-Zalways-encode-mir` (like Miri and Kani do) and see...
I managed to reuse miri to get a usable full-MIR std! Here's what I tried: - `rustup component add miri`; - `cargo miri setup -v --print-sysroot` builds a std with...
I'd like Charon to do this automatically eventually
Closing in favor of https://github.com/AeneasVerif/charon/issues/865 which contains instructions.
This overall looks good, the one issue is the new panic. In the future please don't submit PRs with such regressions without explaining them. Also just so you know the...
Haven't reviewed everything but from what I've seen: could you change how we represent the existential predicates? The current encoding will cause issues with generics (see inline comments).
Could you add a lot of tests please? We need to cover edge cases even if we don't support them yet (write `//@ known-failure` at the top for these cases)....
> Maybe we can focus on the implementation for now? The tests will help me understand what the implementation is doing, I can't just be running the code in my...
For the CI failures, unfortunately I don't know of a good way to normalize the paths, so just add `//@ no-check-output` to those test files.