Nadrieril
Nadrieril
Creusot defines a proc-macro for their `#[ensures]`/`#[invariant]` etc attributes. That's one of the options available (and you started doing something like that with the `attributes` crate).
`register_tool` is the simplest right now. I've heard discussions on the rustc side about what the best design for this feature would be, so I'd suggest using it for now...
https://github.com/AeneasVerif/charon/pull/227 allows the attribute on definitions; it would be nice to also allow the attribute on modules.
These attributes are supported on modules since one of the recent PRs that overhauled opaque handling.
Oh interesting, it seems the boolean condition just isn't computed and it's all done via control flow instead. That's not easy to reconstruct 🤔
Yeah, I want to emit something like: ```rust if e1 { b = e2; } else { b = false; } if b { e3 } else { e4 }...
Here is a sketch of what needs to happen to solve this issue. External help is welcome here. What I need to know is what happens if instead of `mir_built`...
> I would make this pass optional Yes that pass would be optional. It is useful for tools targeting safe rust, for which there should be no raw pointers if...
> from my understanding there is now work done inside the rust compiler that does export [lifetime] information, but not sure how easy to use If there is such work,...
Hm, get_body_with_borrowck_facts has existed for a while, I remember hearing that this wasn't sufficient. For example, this works only on promoted MIR, which is lacking elaborated drops. And I was...