Don't assign comments to fake_read

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<usize, Span> = 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)

charon/tests/ui/comments.out

@@ -44,13 +44,13 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice<u32>)) -> u32
     let @25: &'_ (Slice<u32>); // 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)