Nadrieril
Nadrieril
Hmm, it would be nice if patterns for the impl could also match on the methods
Alright, I understand what's up, I'm working on a fix
This is proving to be a rabbit-hole of a fix. I'll get there eventually but I have to clarify our use of generics some more first.
Alright, thanks to https://github.com/AeneasVerif/charon/pull/468 I was able to adapt the name matcher so that it keeps matching methods identically after we inline them.
My current list: - [x] `Var` -> `Local`: https://github.com/AeneasVerif/charon/pull/645 - [x] `RawStatement` -> `StatementKind` https://github.com/AeneasVerif/charon/pull/805 - [x] `RawTerminator` -> `TerminatorKind` https://github.com/AeneasVerif/charon/pull/805 - [x] `RawConstantExpr` -> `ConstantExprKind` https://github.com/AeneasVerif/charon/pull/805 - [x] `Statement.content`...
Does it output something with `--errors-as-warnings` in the case you're testing?
Said differently, this is charon working as intended: in my mind, calling `charon` by itself should only produce a well-formed output. `--errors-as-warnings` is the flag that allows it to produce...
Hm I see. I presume what happens is that when we `catch_unwind` a compiler panic, this still eventually causes `run_compiler` to panic because the compiler remembers that it panicked. In...
I re-added the top-level catch_unwind which I hope should fix this, but I did not have a test case at hand for this. Could you confirm we now emit llbc?
Noting here so we don't forget: we likely want `impl ... for ..` to only match traits while `impl ...` can match both traits and types.