Suboptimal placement of comment

[msprotz]

Consider the following function (from mlkem):

pub(crate) fn barrett_reduce_element(value: FieldElement) -> FieldElement {
    // hax_debug_assert!(
    //     i32::from(value) > -BARRETT_R && i32::from(value) < BARRETT_R,
    //     "value is {value}"
    // );

    let t = (i32::from(value) * BARRETT_MULTIPLIER) + (BARRETT_R >> 1);
    ...

If I dump what I receive from Charon, the comment is attached to the intermediary (unnamed) value that MIR introduces for i32::from(value) (which internally is just value), or more specifically:

// pseudo-MIR
fn barrett_...(...) {
... lots of variable declarations
i32 t; // this is the user-provided name
... lots of variable declarations
i32 tmp; // internal MIR name
... lots more variable declarations
<<comment attached to the assignment below>>
tmp := value;

I would expect the comment to be attached either to
i) the declaration i32 t; or ii) the assignment into t that comes further down (not modeled in the snippet above).

Right now, Eurydice tracks the location of the comment all the way down to C, re-inlines the temporary computations, and produces something unsightly:

  int32_t
  t =
    (int32_t)/*
    hax_debug_assert!(
    i32::from(value) > -BARRETT_R && i32::from(value) < BARRETT_R,
    "value is {value}"
    );
    */
      value

notice how the comment is attached to the inner value, per the original LLBC received from Charon. Thank you!

[msprotz]

initially spotted by @franziskuskiefer

[Nadrieril]

Right now I assign each comment to the first MIR statement that has a matching span. Maybe I should choose the last one instead? I expect that being more precise than that will be hard because I can't inspect the original syntax.

[Nadrieril]

Nevermind I can do better