Feature request: carry comments in the middle of function bodies down to LLBC

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification

Apache License 2.0

79 stars 14 forks source link

Feature request: carry comments in the middle of function bodies down to LLBC #340

Closed msprotz closed 2 weeks ago

msprotz commented 1 month ago

In the following snippet, I would like a way to retrieve the comment in LLBC.

fn foo() -> u32 {
 // Bar
  0
}

Possible thoughts include:

looking up the text via span information
using a rustdoc comment in the hope that it gets attached to an AST node
...?

Thanks!

Nadrieril commented 1 month ago

Turns out clippy has a lint that detects // SAFETY comments before unsafe blocks. They do span shenanigans to recover the comments. Code is here for inspiration.

Nadrieril commented 2 weeks ago

I made a decent attempt here: https://github.com/AeneasVerif/charon/pull/358, which is made mostly pointless by #233.

Nadrieril commented 2 weeks ago

Alright, this now works! Comments on each statement are accessible in comments_before.

The heuristic for where to place comments is quite naive however, so please report back if comments end up in surprising places.