diff --git a/charon/src/transform/recover_body_comments.rs b/charon/src/transform/recover_body_comments.rs index ff94ea11d..58fda041a 100644 --- a/charon/src/transform/recover_body_comments.rs +++ b/charon/src/transform/recover_body_comments.rs @@ -21,6 +21,10 @@ impl LlbcPass for Transform { // correspond to what the comment was intended to point to. let mut best_span_for_line: HashMap = Default::default(); b.body.drive(&mut visitor_enter_fn(|st: &Statement| { + if matches!(st.content, RawStatement::FakeRead(_)) { + // These are added after many `let` statements and mess up the comments. + return; + } let span = st.span; best_span_for_line .entry(span.span.beg.line) diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out index d0c00b64e..7d47aa527 100644 --- a/charon/tests/ui/comments.out +++ b/charon/tests/ui/comments.out @@ -44,13 +44,13 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice)) -> u32 let @25: &'_ (Slice); // anonymous local let @26: &'_ (u32); // anonymous local - sum@2 := const (0 : u32) // `let sum` + sum@2 := const (0 : u32) @fake_read(sum@2) - i@3 := const (0 : usize) // `let i` // indented sub-comment // unindented sub-comment + i@3 := const (0 : usize) @fake_read(i@3) @6 := copy (sum@2) @5 := move (@6) + const (2 : u32) @@ -218,8 +218,8 @@ fn test_crate::foo() @4 := test_crate::eat_foo(move (@5)) drop @5 drop @4 - a@8 := @ArrayRepeat<'_, u32, 10 : usize>(const (0 : u32)) // Build an array + a@8 := @ArrayRepeat<'_, u32, 10 : usize>(const (0 : u32)) @fake_read(a@8) @12 := const (9 : usize) @29 := &a@8 @@ -291,9 +291,9 @@ fn test_crate::thing() @5 := test_crate::CONSTANT @2 := move (@5) >> const (3 : i32) + // This comment belongs above the assignment to `x` and not above intermediate computations. x@1 := move (@2) + const (12 : u32) drop @2 - // This comment belongs above the assignment to `x` and not above intermediate computations. @fake_read(x@1) @4 := copy (x@1) @3 := test_crate::function_call(move (@4)) @@ -312,7 +312,6 @@ fn test_crate::fake_read(@1: u32) let x@1: u32; // arg #1 let @2: (); // anonymous local - // This statement is translated to a `fake_read`. @fake_read(x@1) @2 := () @0 := move (@2)