From 56d438ffe56260a30c19c8d6ed4b99a98e0ec65b Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Tue, 1 Oct 2024 10:29:50 +0200
Subject: [PATCH] Don't assign comments to `fake_read`

---
 charon/src/transform/recover_body_comments.rs | 4 ++++
 charon/tests/ui/comments.out                  | 7 +++----
 2 files changed, 7 insertions(+), 4 deletions(-)

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<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)
diff --git a/charon/tests/ui/comments.out b/charon/tests/ui/comments.out
index c0e9bb71f..71a4991bf 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>)) -> u32
     let @25: &'_ (Slice<u32>); // anonymous local
     let @26: &'_ (u32); // anonymous local
 
-    sum@2 := const (0 : u32)
     // Comment1
+    sum@2 := const (0 : u32)
     @fake_read(sum@2)
-    i@3 := const (0 : usize)
     // Comment2
     //  Comment2.1
     // Comment2.2
+    i@3 := const (0 : usize)
     @fake_read(i@3)
     @6 := copy (sum@2)
     @5 := move (@6) + const (2 : u32)
@@ -147,9 +147,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))
@@ -168,7 +168,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)