From d2463086182f5487ddccd7e7ce2368a3da486241 Mon Sep 17 00:00:00 2001
From: Vincent Lafeychine <vincent.lafeychine@proton.me>
Date: Wed, 17 Apr 2024 11:18:14 +0200
Subject: [PATCH] chore(analysis): Update test_cases from upstream

---
 .../definitely_accessible/expired.stdout      |   2 +-
 .../definitely_accessible/fields.rs           |   2 +
 .../definitely_accessible/fields.stdout       | 134 +++++++++------
 .../definitely_accessible/infinite_list.rs    |   2 +-
 .../infinite_list.stdout                      |  90 ++++++----
 .../definitely_accessible/ref_field.stdout    |   6 +-
 .../test_cases/definitely_initialized/abs.rs  |   8 +-
 .../definitely_initialized/abs.stdout         |  24 ++-
 .../definitely_initialized/array.rs           |   2 +
 .../definitely_initialized/array.stdout       |   4 +-
 .../definitely_initialized/calls.rs           |   2 +-
 .../definitely_initialized/fields.rs          |   2 +
 .../definitely_initialized/fields.stdout      |  97 +++++++----
 .../repeated_assignment.rs                    |   5 +-
 .../repeated_assignment.stdout                |  27 +--
 .../very_simple_assignment.rs                 |   1 -
 .../tests/test_cases/framing/ref_field.stdout |   6 +-
 .../framing/rust_issue_63787.stdout           |   8 +-
 .../gen_accessibility/basic-move.rs           |   4 +-
 .../gen_accessibility/consume-call.rs         |   6 +-
 .../gen_accessibility/create-box.rs           |   3 +-
 .../test_cases/gen_accessibility/deref.rs     |   5 +-
 .../expiring-loans/borrow-die-with-magic.rs   |   4 +-
 .../gen_accessibility/field-types.rs          |  10 +-
 .../test_cases/gen_accessibility/join.rs      |   2 +-
 .../gen_accessibility/loops/break-continue.rs |   1 -
 .../gen_accessibility/loops/tmp-in-guard.rs   |  18 +-
 .../gen_accessibility/multiple-branches.rs    |  18 +-
 .../gen_accessibility/nll-rfc/message.rs      |   3 +-
 .../gen_accessibility/predicate-old-expr.rs   |   5 +-
 .../gen_accessibility/reassignment.rs         |   5 +-
 .../test_cases/gen_accessibility/structs.rs   |  12 +-
 .../test_cases/maybe_borrowed/linked_list.rs  |   2 +-
 .../maybe_borrowed/linked_list.stdout         |   6 +-
 .../test_cases/reaching_definitions/abs.rs    |   8 +-
 .../reaching_definitions/abs.stdout           | 157 ++++++++++--------
 .../test_cases/reaching_definitions/calls.rs  |   2 +-
 .../repeated_assignment.rs                    |   5 +-
 .../repeated_assignment.stdout                | 125 ++++++++------
 .../relaxed_definitely_initialized/abs.rs     |   6 +-
 .../relaxed_definitely_initialized/abs.stdout |  38 +++--
 41 files changed, 512 insertions(+), 355 deletions(-)

diff --git a/rr_frontend/analysis/tests/test_cases/definitely_accessible/expired.stdout b/rr_frontend/analysis/tests/test_cases/definitely_accessible/expired.stdout
index 7b59accc..6375b524 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_accessible/expired.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_accessible/expired.stdout
@@ -438,7 +438,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb6",
+    "terminator: drop(_1) -> [return: bb6, unwind terminate(cleanup)]",
     {
       "bb6": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.rs b/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.rs
index 0ae84f1b..bcbc0bf2 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.rs
@@ -1,3 +1,5 @@
+#![allow(dropping_references)]
+
 #[derive(Clone, Default)]
 struct T {
     // Wrap in Box to have non-Copy types
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.stdout b/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.stdout
index 758c7279..6106b9d1 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_accessible/fields.stdout
@@ -589,30 +589,51 @@ Result for function main():
         "_11"
       ]
     },
-    "terminator: replace((_1.0: std::boxed::Box<u32>) <- move _11) -> [return: bb6, unwind: bb11]",
+    "terminator: drop((_1.0: std::boxed::Box<u32>)) -> [return: bb6, unwind: bb7]",
     {
-      "bb11": [
-        "state:",
-        {
-          "accessible": [],
-          "owned": []
-        }
-      ],
       "bb6": [
         "state:",
         {
           "accessible": [
-            "_1"
+            "(_1.1: std::boxed::Box<u32>)",
+            "(_1.2: std::boxed::Box<u32>)",
+            "_11"
           ],
           "owned": [
-            "_1"
+            "(_1.1: std::boxed::Box<u32>)",
+            "(_1.2: std::boxed::Box<u32>)",
+            "_11"
           ]
         }
+      ],
+      "bb7": [
+        "state:",
+        {
+          "accessible": [],
+          "owned": []
+        }
       ]
     }
   ],
   "bb6": [
-    [],
+    [
+      [
+        "state:",
+        {
+          "accessible": [
+            "(_1.1: std::boxed::Box<u32>)",
+            "(_1.2: std::boxed::Box<u32>)",
+            "_11"
+          ],
+          "owned": [
+            "(_1.1: std::boxed::Box<u32>)",
+            "(_1.2: std::boxed::Box<u32>)",
+            "_11"
+          ]
+        },
+        "statement: (_1.0: std::boxed::Box<u32>) = move _11"
+      ]
+    ],
     "state before terminator:",
     {
       "accessible": [
@@ -622,7 +643,7 @@ Result for function main():
         "_1"
       ]
     },
-    "terminator: drop(_11) -> [return: bb7, unwind: bb13]",
+    "terminator: drop(_11) -> [return: bb8, unwind: bb13]",
     {
       "bb13": [
         "state:",
@@ -631,7 +652,7 @@ Result for function main():
           "owned": []
         }
       ],
-      "bb7": [
+      "bb8": [
         "state:",
         {
           "accessible": [
@@ -645,6 +666,41 @@ Result for function main():
     }
   ],
   "bb7": [
+    [
+      [
+        "state:",
+        {
+          "accessible": [],
+          "owned": []
+        },
+        "statement: (_1.0: std::boxed::Box<u32>) = move _11"
+      ]
+    ],
+    "state before terminator:",
+    {
+      "accessible": [
+        "(_1.0: std::boxed::Box<u32>)"
+      ],
+      "owned": [
+        "(_1.0: std::boxed::Box<u32>)"
+      ]
+    },
+    "terminator: drop(_11) -> [return: bb13, unwind terminate(cleanup)]",
+    {
+      "bb13": [
+        "state:",
+        {
+          "accessible": [
+            "(_1.0: std::boxed::Box<u32>)"
+          ],
+          "owned": [
+            "(_1.0: std::boxed::Box<u32>)"
+          ]
+        }
+      ]
+    }
+  ],
+  "bb8": [
     [
       [
         "state:",
@@ -704,16 +760,16 @@ Result for function main():
         "_13"
       ]
     },
-    "terminator: _12 = std::mem::drop::<T>(move _13) -> [return: bb8, unwind: bb10]",
+    "terminator: _12 = std::mem::drop::<T>(move _13) -> [return: bb9, unwind: bb11]",
     {
-      "bb10": [
+      "bb11": [
         "state:",
         {
           "accessible": [],
           "owned": []
         }
       ],
-      "bb8": [
+      "bb9": [
         "state:",
         {
           "accessible": [
@@ -726,7 +782,7 @@ Result for function main():
       ]
     }
   ],
-  "bb8": [
+  "bb9": [
     [
       [
         "state:",
@@ -806,16 +862,9 @@ Result for function main():
         "_0"
       ]
     },
-    "terminator: drop(_1) -> [return: bb9, unwind: bb14]",
+    "terminator: drop(_1) -> [return: bb10, unwind: bb14]",
     {
-      "bb14": [
-        "state:",
-        {
-          "accessible": [],
-          "owned": []
-        }
-      ],
-      "bb9": [
+      "bb10": [
         "state:",
         {
           "accessible": [
@@ -825,10 +874,17 @@ Result for function main():
             "_0"
           ]
         }
+      ],
+      "bb14": [
+        "state:",
+        {
+          "accessible": [],
+          "owned": []
+        }
       ]
     }
   ],
-  "bb9": [
+  "bb10": [
     [
       [
         "state:",
@@ -855,24 +911,6 @@ Result for function main():
     "terminator: return",
     {}
   ],
-  "bb10": [
-    [],
-    "state before terminator:",
-    {
-      "accessible": [],
-      "owned": []
-    },
-    "terminator: drop(_13) -> bb13",
-    {
-      "bb13": [
-        "state:",
-        {
-          "accessible": [],
-          "owned": []
-        }
-      ]
-    }
-  ],
   "bb11": [
     [],
     "state before terminator:",
@@ -880,7 +918,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_11) -> bb13",
+    "terminator: drop(_13) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -898,7 +936,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_3) -> bb13",
+    "terminator: drop(_3) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -916,7 +954,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb14",
+    "terminator: drop(_1) -> [return: bb14, unwind terminate(cleanup)]",
     {
       "bb14": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.rs b/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.rs
index 829f59d0..311e96a5 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.rs
@@ -1,6 +1,6 @@
 struct InfiniteList {
     val: u32,
-    next: Box<InfiniteList>
+    next: Box<InfiniteList>,
 }
 
 #[analyzer::run]
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.stdout b/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.stdout
index 7775daa2..fc383dce 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_accessible/infinite_list.stdout
@@ -164,7 +164,7 @@ Result for function test1():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb4",
+    "terminator: drop(_1) -> [return: bb4, unwind terminate(cleanup)]",
     {
       "bb4": [
         "state:",
@@ -228,20 +228,20 @@ Result for function test2():
         "_2"
       ]
     },
-    "terminator: replace(_1 <- move _2) -> [return: bb1, unwind: bb4]",
+    "terminator: drop(_1) -> [return: bb1, unwind: bb2]",
     {
       "bb1": [
         "state:",
         {
           "accessible": [
-            "_1"
+            "_2"
           ],
           "owned": [
-            "_1"
+            "_2"
           ]
         }
       ],
-      "bb4": [
+      "bb2": [
         "state:",
         {
           "accessible": [],
@@ -251,7 +251,20 @@ Result for function test2():
     }
   ],
   "bb1": [
-    [],
+    [
+      [
+        "state:",
+        {
+          "accessible": [
+            "_2"
+          ],
+          "owned": [
+            "_2"
+          ]
+        },
+        "statement: _1 = move _2"
+      ]
+    ],
     "state before terminator:",
     {
       "accessible": [
@@ -261,9 +274,9 @@ Result for function test2():
         "_1"
       ]
     },
-    "terminator: drop(_2) -> [return: bb2, unwind: bb5]",
+    "terminator: drop(_2) -> [return: bb3, unwind: bb5]",
     {
-      "bb2": [
+      "bb3": [
         "state:",
         {
           "accessible": [
@@ -284,6 +297,41 @@ Result for function test2():
     }
   ],
   "bb2": [
+    [
+      [
+        "state:",
+        {
+          "accessible": [],
+          "owned": []
+        },
+        "statement: _1 = move _2"
+      ]
+    ],
+    "state before terminator:",
+    {
+      "accessible": [
+        "_1"
+      ],
+      "owned": [
+        "_1"
+      ]
+    },
+    "terminator: drop(_2) -> [return: bb5, unwind terminate(cleanup)]",
+    {
+      "bb5": [
+        "state:",
+        {
+          "accessible": [
+            "_1"
+          ],
+          "owned": [
+            "_1"
+          ]
+        }
+      ]
+    }
+  ],
+  "bb3": [
     [
       [
         "state:",
@@ -321,9 +369,9 @@ Result for function test2():
         "_1"
       ]
     },
-    "terminator: drop(_1) -> [return: bb3, unwind: bb6]",
+    "terminator: drop(_1) -> [return: bb4, unwind: bb6]",
     {
-      "bb3": [
+      "bb4": [
         "state:",
         {
           "accessible": [
@@ -343,7 +391,7 @@ Result for function test2():
       ]
     }
   ],
-  "bb3": [
+  "bb4": [
     [],
     "state before terminator:",
     {
@@ -357,24 +405,6 @@ Result for function test2():
     "terminator: return",
     {}
   ],
-  "bb4": [
-    [],
-    "state before terminator:",
-    {
-      "accessible": [],
-      "owned": []
-    },
-    "terminator: drop(_2) -> bb5",
-    {
-      "bb5": [
-        "state:",
-        {
-          "accessible": [],
-          "owned": []
-        }
-      ]
-    }
-  ],
   "bb5": [
     [],
     "state before terminator:",
@@ -382,7 +412,7 @@ Result for function test2():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb6",
+    "terminator: drop(_1) -> [return: bb6, unwind terminate(cleanup)]",
     {
       "bb6": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_accessible/ref_field.stdout b/rr_frontend/analysis/tests/test_cases/definitely_accessible/ref_field.stdout
index 7cd44ae9..cdbfd0ec 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_accessible/ref_field.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_accessible/ref_field.stdout
@@ -939,7 +939,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_16) -> bb10",
+    "terminator: drop(_16) -> [return: bb10, unwind terminate(cleanup)]",
     {
       "bb10": [
         "state:",
@@ -957,7 +957,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_1) -> bb12",
+    "terminator: drop(_1) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",
@@ -975,7 +975,7 @@ Result for function main():
       "accessible": [],
       "owned": []
     },
-    "terminator: drop(_2) -> bb12",
+    "terminator: drop(_2) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.rs b/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.rs
index 3827da56..e70e687a 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.rs
@@ -1,8 +1,7 @@
-
 fn main() {
     let a = abs(-1);
     let b = abs(1);
-    println!("{}", a+b);
+    println!("{}", a + b);
 }
 
 #[analyzer::run]
@@ -10,9 +9,8 @@ fn abs(x: i32) -> i32 {
     let res: i32;
     if x >= 0 {
         res = x;
-    }
-    else {
+    } else {
         res = -x;
     }
     return res;
-}
\ No newline at end of file
+}
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.stdout b/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.stdout
index 430d23f4..47c616c4 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/abs.stdout
@@ -45,14 +45,6 @@ Result for function abs():
           "_6"
         ],
         "statement: _5 = Ge(move _6, const 0_i32)"
-      ],
-      [
-        "state:",
-        [
-          "_1",
-          "_5"
-        ],
-        "statement: StorageDead(_6)"
       ]
     ],
     "state before terminator:",
@@ -60,7 +52,7 @@ Result for function abs():
       "_1",
       "_5"
     ],
-    "terminator: switchInt(move _5) -> [false: bb2, otherwise: bb1]",
+    "terminator: switchInt(move _5) -> [0: bb2, otherwise: bb1]",
     {
       "bb1": [
         "state:",
@@ -78,6 +70,13 @@ Result for function abs():
   ],
   "bb1": [
     [
+      [
+        "state:",
+        [
+          "_1"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
@@ -137,6 +136,13 @@ Result for function abs():
   ],
   "bb2": [
     [
+      [
+        "state:",
+        [
+          "_1"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.rs b/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.rs
index a128f7b3..ce548896 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.rs
@@ -1,3 +1,5 @@
+#![allow(dropping_copy_types)]
+
 #[analyzer::run]
 fn main() {
     let x = [1, 2, 3];
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.stdout b/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.stdout
index 58413271..4aceb239 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/array.stdout
@@ -284,7 +284,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_7) -> bb7",
+    "terminator: drop(_7) -> [return: bb7, unwind terminate(cleanup)]",
     {
       "bb7": [
         "state:",
@@ -296,7 +296,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_4) -> bb8",
+    "terminator: drop(_4) -> [return: bb8, unwind terminate(cleanup)]",
     {
       "bb8": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/calls.rs b/rr_frontend/analysis/tests/test_cases/definitely_initialized/calls.rs
index 0c6e1153..a9dadb0c 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/calls.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/calls.rs
@@ -9,4 +9,4 @@ fn main() {
 
 fn f(x: i32) -> i32 {
     return x;
-}
\ No newline at end of file
+}
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.rs b/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.rs
index daad1c00..dda348eb 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.rs
@@ -1,3 +1,5 @@
+#![allow(dropping_references)]
+
 #[derive(Clone, Default)]
 struct T {
     // Wrap in box to have non-Copy types
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.stdout b/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.stdout
index 60a4e310..75b4c0bf 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/fields.stdout
@@ -408,25 +408,40 @@ Result for function main():
       "_6",
       "_11"
     ],
-    "terminator: replace((_1.0: std::boxed::Box<u32>) <- move _11) -> [return: bb6, unwind: bb11]",
+    "terminator: drop((_1.0: std::boxed::Box<u32>)) -> [return: bb6, unwind: bb7]",
     {
-      "bb11": [
-        "state:",
-        []
-      ],
       "bb6": [
         "state:",
         [
-          "_1",
+          "(_1.1: std::boxed::Box<u32>)",
+          "(_1.2: std::boxed::Box<u32>)",
           "_4",
           "_5",
-          "_6"
+          "_6",
+          "_11"
         ]
+      ],
+      "bb7": [
+        "state:",
+        []
       ]
     }
   ],
   "bb6": [
-    [],
+    [
+      [
+        "state:",
+        [
+          "(_1.1: std::boxed::Box<u32>)",
+          "(_1.2: std::boxed::Box<u32>)",
+          "_4",
+          "_5",
+          "_6",
+          "_11"
+        ],
+        "statement: (_1.0: std::boxed::Box<u32>) = move _11"
+      ]
+    ],
     "state before terminator:",
     [
       "_1",
@@ -434,13 +449,13 @@ Result for function main():
       "_5",
       "_6"
     ],
-    "terminator: drop(_11) -> [return: bb7, unwind: bb13]",
+    "terminator: drop(_11) -> [return: bb8, unwind: bb13]",
     {
       "bb13": [
         "state:",
         []
       ],
-      "bb7": [
+      "bb8": [
         "state:",
         [
           "_1",
@@ -452,6 +467,28 @@ Result for function main():
     }
   ],
   "bb7": [
+    [
+      [
+        "state:",
+        [],
+        "statement: (_1.0: std::boxed::Box<u32>) = move _11"
+      ]
+    ],
+    "state before terminator:",
+    [
+      "(_1.0: std::boxed::Box<u32>)"
+    ],
+    "terminator: drop(_11) -> [return: bb13, unwind terminate(cleanup)]",
+    {
+      "bb13": [
+        "state:",
+        [
+          "(_1.0: std::boxed::Box<u32>)"
+        ]
+      ]
+    }
+  ],
+  "bb8": [
     [
       [
         "state:",
@@ -501,13 +538,13 @@ Result for function main():
       "_6",
       "_13"
     ],
-    "terminator: _12 = std::mem::drop::<T>(move _13) -> [return: bb8, unwind: bb10]",
+    "terminator: _12 = std::mem::drop::<T>(move _13) -> [return: bb9, unwind: bb11]",
     {
-      "bb10": [
+      "bb11": [
         "state:",
         []
       ],
-      "bb8": [
+      "bb9": [
         "state:",
         [
           "_4",
@@ -518,7 +555,7 @@ Result for function main():
       ]
     }
   ],
-  "bb8": [
+  "bb9": [
     [
       [
         "state:",
@@ -581,21 +618,21 @@ Result for function main():
     [
       "_0"
     ],
-    "terminator: drop(_1) -> [return: bb9, unwind: bb14]",
+    "terminator: drop(_1) -> [return: bb10, unwind: bb14]",
     {
-      "bb14": [
-        "state:",
-        []
-      ],
-      "bb9": [
+      "bb10": [
         "state:",
         [
           "_0"
         ]
+      ],
+      "bb14": [
+        "state:",
+        []
       ]
     }
   ],
-  "bb9": [
+  "bb10": [
     [
       [
         "state:",
@@ -612,23 +649,11 @@ Result for function main():
     "terminator: return",
     {}
   ],
-  "bb10": [
-    [],
-    "state before terminator:",
-    [],
-    "terminator: drop(_13) -> bb13",
-    {
-      "bb13": [
-        "state:",
-        []
-      ]
-    }
-  ],
   "bb11": [
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_11) -> bb13",
+    "terminator: drop(_13) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -640,7 +665,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_3) -> bb13",
+    "terminator: drop(_3) -> [return: bb13, unwind terminate(cleanup)]",
     {
       "bb13": [
         "state:",
@@ -652,7 +677,7 @@ Result for function main():
     [],
     "state before terminator:",
     [],
-    "terminator: drop(_1) -> bb14",
+    "terminator: drop(_1) -> [return: bb14, unwind terminate(cleanup)]",
     {
       "bb14": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.rs b/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.rs
index 29875ea2..007a91d8 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.rs
@@ -5,8 +5,7 @@ fn main() {
     x = input();
     if x > 2 {
         y = 5;
-    }
-    else {
+    } else {
         y = 7;
     }
     y = 25;
@@ -14,4 +13,4 @@ fn main() {
 
 fn input() -> i32 {
     return 42;
-}
\ No newline at end of file
+}
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout b/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout
index b15a1abb..87be870a 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout
@@ -131,15 +131,6 @@ Result for function main():
           "_6"
         ],
         "statement: _5 = Gt(move _6, const 2_i32)"
-      ],
-      [
-        "state:",
-        [
-          "_1",
-          "_2",
-          "_5"
-        ],
-        "statement: StorageDead(_6)"
       ]
     ],
     "state before terminator:",
@@ -148,7 +139,7 @@ Result for function main():
       "_2",
       "_5"
     ],
-    "terminator: switchInt(move _5) -> [false: bb3, otherwise: bb2]",
+    "terminator: switchInt(move _5) -> [0: bb3, otherwise: bb2]",
     {
       "bb2": [
         "state:",
@@ -168,6 +159,14 @@ Result for function main():
   ],
   "bb2": [
     [
+      [
+        "state:",
+        [
+          "_1",
+          "_2"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
@@ -205,6 +204,14 @@ Result for function main():
   ],
   "bb3": [
     [
+      [
+        "state:",
+        [
+          "_1",
+          "_2"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
diff --git a/rr_frontend/analysis/tests/test_cases/definitely_initialized/very_simple_assignment.rs b/rr_frontend/analysis/tests/test_cases/definitely_initialized/very_simple_assignment.rs
index 287199cf..a3771f91 100644
--- a/rr_frontend/analysis/tests/test_cases/definitely_initialized/very_simple_assignment.rs
+++ b/rr_frontend/analysis/tests/test_cases/definitely_initialized/very_simple_assignment.rs
@@ -4,4 +4,3 @@ fn main() {
     let y: u32;
     y = x;
 }
-
diff --git a/rr_frontend/analysis/tests/test_cases/framing/ref_field.stdout b/rr_frontend/analysis/tests/test_cases/framing/ref_field.stdout
index 61ac9657..47c265d6 100644
--- a/rr_frontend/analysis/tests/test_cases/framing/ref_field.stdout
+++ b/rr_frontend/analysis/tests/test_cases/framing/ref_field.stdout
@@ -529,7 +529,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_9) -> bb10",
+    "terminator: drop(_9) -> [return: bb10, unwind terminate(cleanup)]",
     {
       "bb10": [
         "state:",
@@ -547,7 +547,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_1) -> bb12",
+    "terminator: drop(_1) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",
@@ -565,7 +565,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_2) -> bb12",
+    "terminator: drop(_2) -> [return: bb12, unwind terminate(cleanup)]",
     {
       "bb12": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/framing/rust_issue_63787.stdout b/rr_frontend/analysis/tests/test_cases/framing/rust_issue_63787.stdout
index a1574869..74fb6889 100644
--- a/rr_frontend/analysis/tests/test_cases/framing/rust_issue_63787.stdout
+++ b/rr_frontend/analysis/tests/test_cases/framing/rust_issue_63787.stdout
@@ -350,7 +350,7 @@ Result for function break_it():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_7) -> bb8",
+    "terminator: drop(_7) -> [return: bb8, unwind terminate(cleanup)]",
     {
       "bb8": [
         "state:",
@@ -368,7 +368,7 @@ Result for function break_it():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_4) -> bb8",
+    "terminator: drop(_4) -> [return: bb8, unwind terminate(cleanup)]",
     {
       "bb8": [
         "state:",
@@ -386,7 +386,7 @@ Result for function break_it():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_2) -> bb9",
+    "terminator: drop(_2) -> [return: bb9, unwind terminate(cleanup)]",
     {
       "bb9": [
         "state:",
@@ -688,7 +688,7 @@ Result for function main():
       "frame_accessible": [],
       "frame_owned": []
     },
-    "terminator: drop(_4) -> bb5",
+    "terminator: drop(_4) -> [return: bb5, unwind terminate(cleanup)]",
     {
       "bb5": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/basic-move.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/basic-move.rs
index 8ffcc336..abc3e4af 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/basic-move.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/basic-move.rs
@@ -3,9 +3,7 @@ pub struct S2 {
 }
 
 pub fn test4() -> S2 {
-    let x = S2 {
-        f: 8,
-    };
+    let x = S2 { f: 8 };
     let y = x;
     assert!(y.f == 9);
     y
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/consume-call.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/consume-call.rs
index 4ac2404c..e8455a07 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/consume-call.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/consume-call.rs
@@ -1,13 +1,13 @@
 struct A;
 struct B {
     a1: A,
-    a2: A
+    a2: A,
 }
 struct C {
-    b: B
+    b: B,
 }
 struct D {
-    c: C
+    c: C,
 }
 
 fn consume(a: A) {}
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/create-box.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/create-box.rs
index d66e6a40..3e7e389e 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/create-box.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/create-box.rs
@@ -1,5 +1,4 @@
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 fn use_box(v: i32) -> Box<i32> {
     let x = Box::new(v);
@@ -7,6 +6,6 @@ fn use_box(v: i32) -> Box<i32> {
     assert!(v == y);
     let z = Box::new(y);
     assert!(v == *z);
-    let result = box *z;
+    let result = Box::new(*z);
     result
 }
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/deref.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/deref.rs
index 2753cce0..030be55c 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/deref.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/deref.rs
@@ -1,8 +1,7 @@
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 struct InfiniteList1 {
-    next: Box<InfiniteList1>
+    next: Box<InfiniteList1>,
 }
 
 fn consume1(x: InfiniteList1) {}
@@ -15,7 +14,7 @@ fn reassignment1(mut x: InfiniteList1) {
 
 struct InfiniteList2 {
     val: u32,
-    next: Box<InfiniteList2>
+    next: Box<InfiniteList2>,
 }
 
 fn consume2(x: InfiniteList2) {}
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/expiring-loans/borrow-die-with-magic.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/expiring-loans/borrow-die-with-magic.rs
index cb18a536..f9239188 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/expiring-loans/borrow-die-with-magic.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/expiring-loans/borrow-die-with-magic.rs
@@ -11,7 +11,9 @@ fn consume_F(_f: F) {}
 
 fn use_both(_f: &mut G, _g: &mut G) {}
 
-fn either<'a>(f: &'a mut G, _g: &'a mut G) -> &'a mut G { f }
+fn either<'a>(f: &'a mut G, _g: &'a mut G) -> &'a mut G {
+    f
+}
 
 fn test3(y: &mut F) {
     let x = &mut *y;
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/field-types.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/field-types.rs
index f9754065..7bbc6ce0 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/field-types.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/field-types.rs
@@ -1,19 +1,21 @@
 struct A {
-    val: i32
+    val: i32,
 }
 
 struct B {
-    val: bool
+    val: bool,
 }
 
 struct C {
-    val: A
+    val: A,
 }
 
 fn main() {
     let mut a = A { val: 111 };
     let mut b = B { val: true };
-    let mut c = C { val: A { val: 222 } };
+    let mut c = C {
+        val: A { val: 222 },
+    };
     a.val = 333;
     b.val = false;
     c.val.val = 444;
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/join.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/join.rs
index 48af8f24..61ff2836 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/join.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/join.rs
@@ -1,6 +1,6 @@
 struct MyStruct {
     a: i32,
-    b: (i32, i32)
+    b: (i32, i32),
 }
 
 fn foo(mut x: MyStruct, switch: bool) -> MyStruct {
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/break-continue.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/break-continue.rs
index 5b768552..708cec24 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/break-continue.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/break-continue.rs
@@ -1,4 +1,3 @@
-
 fn random(i: u32) -> bool {
     unimplemented!()
 }
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs
index c1f0cd85..f46d252a 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/loops/tmp-in-guard.rs
@@ -1,53 +1,51 @@
-#![feature(box_syntax)]
-
 fn random() -> u32 {
     unimplemented!()
 }
 
 fn test1() {
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
     while {
         let guard = random() < 55;
 
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
 
         guard
     } {
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
     }
 
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 }
 
 fn test2() {
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 
     while {
         let guard = random() < 55;
 
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
 
         guard
     } {
-        let mut tmp = box box random();
+        let mut tmp = Box::new(Box::new(random()));
         let tmp_ref = &tmp;
         let tmp_ref_mut = &mut tmp;
     }
 
-    let mut tmp = box box random();
+    let mut tmp = Box::new(Box::new(random()));
     let tmp_ref = &tmp;
     let tmp_ref_mut = &mut tmp;
 }
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/multiple-branches.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/multiple-branches.rs
index e96e45b3..f5d43fdc 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/multiple-branches.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/multiple-branches.rs
@@ -1,13 +1,19 @@
 struct MyStruct {
     a: i32,
-    b: (i32, i32)
+    b: (i32, i32),
 }
 
 fn foo(switch: bool) -> MyStruct {
-    let mut x = MyStruct { a: 000, b: (000, 000) };
-    let y = MyStruct { a: 111, b: (222, 333) };
+    let mut x = MyStruct {
+        a: 000,
+        b: (000, 000),
+    };
+    let y = MyStruct {
+        a: 111,
+        b: (222, 333),
+    };
     if switch {
-        return x
+        return x;
     }
     if switch {
         x.b.0 = 444;
@@ -16,7 +22,7 @@ fn foo(switch: bool) -> MyStruct {
         x.b.1 = 555;
     }
     if switch {
-        return x
+        return x;
     }
     if switch {
         x.a = 666;
@@ -25,7 +31,7 @@ fn foo(switch: bool) -> MyStruct {
         x.b = (777, 888);
     }
     if switch {
-        return x
+        return x;
     }
     if switch {
         x.a = y.a;
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/nll-rfc/message.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/nll-rfc/message.rs
index 681937fd..a52e7276 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/nll-rfc/message.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/nll-rfc/message.rs
@@ -3,7 +3,6 @@
 ///
 /// which was created by Matsakis to show-case NLL in his blog:
 /// http://smallcultfollowing.com/babysteps/blog/2018/10/31/mir-based-borrowck-is-almost-here/
-
 use std::sync::mpsc::{Receiver, Sender};
 
 enum Message {
@@ -19,7 +18,7 @@ fn router(me: &str, rx: Receiver<Message>, tx: Sender<Message>) {
                 } else {
                     process(data);
                 }
-            }
+            },
         }
     }
 }
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs
index 5ea34767..c8a22d66 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/predicate-old-expr.rs
@@ -1,5 +1,4 @@
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 use std::borrow::BorrowMut;
 
@@ -16,10 +15,10 @@ fn lookup(head: &List, index: usize) -> u32 {
         match head.next {
             Some(box ref tail) => {
                 result = lookup(tail, index - 1);
-            }
+            },
             None => {
                 unreachable!();
-            }
+            },
         }
     }
     result
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/reassignment.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/reassignment.rs
index 3bf58abb..5e6917df 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/reassignment.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/reassignment.rs
@@ -1,11 +1,10 @@
 //! Example of reassignment
 
 #![feature(box_patterns)]
-#![feature(box_syntax)]
 
 struct InfiniteList {
     val: i32,
-    next: Box<InfiniteList>
+    next: Box<InfiniteList>,
 }
 
 fn consume(x: InfiniteList) {}
@@ -16,5 +15,5 @@ fn reassignment(a: InfiniteList) {
     // Reassignment
     x = *(*(*(*(*x.next).next).next).next).next;
 
-	consume(x);
+    consume(x);
 }
diff --git a/rr_frontend/analysis/tests/test_cases/gen_accessibility/structs.rs b/rr_frontend/analysis/tests/test_cases/gen_accessibility/structs.rs
index 29b29cd7..43963bf1 100644
--- a/rr_frontend/analysis/tests/test_cases/gen_accessibility/structs.rs
+++ b/rr_frontend/analysis/tests/test_cases/gen_accessibility/structs.rs
@@ -1,12 +1,18 @@
 struct MyStruct {
     a: i32,
-    b: (i32, i32)
+    b: (i32, i32),
 }
 
 fn foo<'a>(arg: MyStruct) -> (i32, i32) {
-    let mut x = MyStruct { a: 111, b: (222, 333) };
+    let mut x = MyStruct {
+        a: 111,
+        b: (222, 333),
+    };
     x.b.0 = 444;
     let y = x;
-    let z = MyStruct { a: 555, b: (666, 777) };
+    let z = MyStruct {
+        a: 555,
+        b: (666, 777),
+    };
     y.b
 }
diff --git a/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.rs b/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.rs
index 97fff940..dea001fa 100644
--- a/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.rs
+++ b/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.rs
@@ -2,7 +2,7 @@
 
 struct Node {
     value: u32,
-    next: Option<Box<Node>>
+    next: Option<Box<Node>>,
 }
 
 #[analyzer::run]
diff --git a/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.stdout b/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.stdout
index eb3d0539..c70dc6f1 100644
--- a/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.stdout
+++ b/rr_frontend/analysis/tests/test_cases/maybe_borrowed/linked_list.stdout
@@ -162,7 +162,7 @@ Result for function borrow_fields():
       "frozen": [],
       "blocked": []
     },
-    "terminator: drop(_1) -> bb4",
+    "terminator: drop(_1) -> [return: bb4, unwind terminate(cleanup)]",
     {
       "bb4": [
         "state:",
@@ -252,7 +252,7 @@ Result for function last_val_mut():
       "frozen": [],
       "blocked": []
     },
-    "terminator: falseUnwind -> [real: bb2, cleanup: bb6]",
+    "terminator: falseUnwind -> [real: bb2, unwind: bb6]",
     {
       "bb2": [
         "state:",
@@ -316,7 +316,7 @@ Result for function last_val_mut():
         "_3"
       ]
     },
-    "terminator: switchInt(move _7) -> [1_isize: bb3, otherwise: bb5]",
+    "terminator: switchInt(move _7) -> [1: bb3, otherwise: bb5]",
     {
       "bb3": [
         "state:",
diff --git a/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.rs b/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.rs
index 3827da56..e70e687a 100644
--- a/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.rs
+++ b/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.rs
@@ -1,8 +1,7 @@
-
 fn main() {
     let a = abs(-1);
     let b = abs(1);
-    println!("{}", a+b);
+    println!("{}", a + b);
 }
 
 #[analyzer::run]
@@ -10,9 +9,8 @@ fn abs(x: i32) -> i32 {
     let res: i32;
     if x >= 0 {
         res = x;
-    }
-    else {
+    } else {
         res = -x;
     }
     return res;
-}
\ No newline at end of file
+}
diff --git a/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.stdout b/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.stdout
index 5caa8241..2aab0969 100644
--- a/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.stdout
+++ b/rr_frontend/analysis/tests/test_cases/reaching_definitions/abs.stdout
@@ -59,21 +59,6 @@ Result for function abs():
           ]
         },
         "statement: _5 = Ge(move _6, const 0_i32)"
-      ],
-      [
-        "state:",
-        {
-          "_1": [
-            "arg0"
-          ],
-          "_5": [
-            "bb0[5]: _5 = Ge(move _6, const 0_i32)"
-          ],
-          "_6": [
-            "bb0[4]: _6 = _1"
-          ]
-        },
-        "statement: StorageDead(_6)"
       ]
     ],
     "state before terminator:",
@@ -88,7 +73,7 @@ Result for function abs():
         "bb0[4]: _6 = _1"
       ]
     },
-    "terminator: switchInt(move _5) -> [false: bb2, otherwise: bb1]",
+    "terminator: switchInt(move _5) -> [0: bb2, otherwise: bb1]",
     {
       "bb1": [
         "state:",
@@ -122,6 +107,21 @@ Result for function abs():
   ],
   "bb1": [
     [
+      [
+        "state:",
+        {
+          "_1": [
+            "arg0"
+          ],
+          "_5": [
+            "bb0[5]: _5 = Ge(move _6, const 0_i32)"
+          ],
+          "_6": [
+            "bb0[4]: _6 = _1"
+          ]
+        },
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         {
@@ -165,7 +165,7 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ]
         },
         "statement: _3 = move _7"
@@ -177,7 +177,7 @@ Result for function abs():
             "arg0"
           ],
           "_3": [
-            "bb1[2]: _3 = move _7"
+            "bb1[3]: _3 = move _7"
           ],
           "_5": [
             "bb0[5]: _5 = Ge(move _6, const 0_i32)"
@@ -186,7 +186,7 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ]
         },
         "statement: StorageDead(_7)"
@@ -198,7 +198,7 @@ Result for function abs():
             "arg0"
           ],
           "_3": [
-            "bb1[2]: _3 = move _7"
+            "bb1[3]: _3 = move _7"
           ],
           "_5": [
             "bb0[5]: _5 = Ge(move _6, const 0_i32)"
@@ -207,7 +207,7 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ]
         },
         "statement: _4 = const ()"
@@ -219,10 +219,10 @@ Result for function abs():
         "arg0"
       ],
       "_3": [
-        "bb1[2]: _3 = move _7"
+        "bb1[3]: _3 = move _7"
       ],
       "_4": [
-        "bb1[4]: _4 = const ()"
+        "bb1[5]: _4 = const ()"
       ],
       "_5": [
         "bb0[5]: _5 = Ge(move _6, const 0_i32)"
@@ -231,7 +231,7 @@ Result for function abs():
         "bb0[4]: _6 = _1"
       ],
       "_7": [
-        "bb1[1]: _7 = _1"
+        "bb1[2]: _7 = _1"
       ]
     },
     "terminator: goto -> bb4",
@@ -243,10 +243,10 @@ Result for function abs():
             "arg0"
           ],
           "_3": [
-            "bb1[2]: _3 = move _7"
+            "bb1[3]: _3 = move _7"
           ],
           "_4": [
-            "bb1[4]: _4 = const ()"
+            "bb1[5]: _4 = const ()"
           ],
           "_5": [
             "bb0[5]: _5 = Ge(move _6, const 0_i32)"
@@ -255,7 +255,7 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ]
         }
       ]
@@ -263,6 +263,21 @@ Result for function abs():
   ],
   "bb2": [
     [
+      [
+        "state:",
+        {
+          "_1": [
+            "arg0"
+          ],
+          "_5": [
+            "bb0[5]: _5 = Ge(move _6, const 0_i32)"
+          ],
+          "_6": [
+            "bb0[4]: _6 = _1"
+          ]
+        },
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         {
@@ -306,7 +321,7 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ]
         },
         "statement: _9 = Eq(_8, const i32::MIN)"
@@ -324,10 +339,10 @@ Result for function abs():
         "bb0[4]: _6 = _1"
       ],
       "_8": [
-        "bb2[1]: _8 = _1"
+        "bb2[2]: _8 = _1"
       ],
       "_9": [
-        "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+        "bb2[3]: _9 = Eq(_8, const i32::MIN)"
       ]
     },
     "terminator: assert(!move _9, /"attempt to negate `{}`, which would overflow/", _8) -> [success: bb3, unwind: bb5]",
@@ -345,10 +360,10 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         }
       ],
@@ -365,10 +380,10 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         }
       ]
@@ -389,10 +404,10 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         },
         "statement: _3 = Neg(move _8)"
@@ -413,10 +428,10 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         },
         "statement: StorageDead(_8)"
@@ -437,10 +452,10 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         },
         "statement: _4 = const ()"
@@ -464,10 +479,10 @@ Result for function abs():
         "bb0[4]: _6 = _1"
       ],
       "_8": [
-        "bb2[1]: _8 = _1"
+        "bb2[2]: _8 = _1"
       ],
       "_9": [
-        "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+        "bb2[3]: _9 = Eq(_8, const i32::MIN)"
       ]
     },
     "terminator: goto -> bb4",
@@ -491,10 +506,10 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         }
       ]
@@ -509,11 +524,11 @@ Result for function abs():
             "arg0"
           ],
           "_3": [
-            "bb1[2]: _3 = move _7",
+            "bb1[3]: _3 = move _7",
             "bb3[0]: _3 = Neg(move _8)"
           ],
           "_4": [
-            "bb1[4]: _4 = const ()",
+            "bb1[5]: _4 = const ()",
             "bb3[2]: _4 = const ()"
           ],
           "_5": [
@@ -523,13 +538,13 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         },
         "statement: StorageDead(_5)"
@@ -541,11 +556,11 @@ Result for function abs():
             "arg0"
           ],
           "_3": [
-            "bb1[2]: _3 = move _7",
+            "bb1[3]: _3 = move _7",
             "bb3[0]: _3 = Neg(move _8)"
           ],
           "_4": [
-            "bb1[4]: _4 = const ()",
+            "bb1[5]: _4 = const ()",
             "bb3[2]: _4 = const ()"
           ],
           "_5": [
@@ -555,13 +570,13 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         },
         "statement: StorageDead(_4)"
@@ -573,11 +588,11 @@ Result for function abs():
             "arg0"
           ],
           "_3": [
-            "bb1[2]: _3 = move _7",
+            "bb1[3]: _3 = move _7",
             "bb3[0]: _3 = Neg(move _8)"
           ],
           "_4": [
-            "bb1[4]: _4 = const ()",
+            "bb1[5]: _4 = const ()",
             "bb3[2]: _4 = const ()"
           ],
           "_5": [
@@ -587,13 +602,13 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         },
         "statement: _0 = _3"
@@ -608,11 +623,11 @@ Result for function abs():
             "arg0"
           ],
           "_3": [
-            "bb1[2]: _3 = move _7",
+            "bb1[3]: _3 = move _7",
             "bb3[0]: _3 = Neg(move _8)"
           ],
           "_4": [
-            "bb1[4]: _4 = const ()",
+            "bb1[5]: _4 = const ()",
             "bb3[2]: _4 = const ()"
           ],
           "_5": [
@@ -622,13 +637,13 @@ Result for function abs():
             "bb0[4]: _6 = _1"
           ],
           "_7": [
-            "bb1[1]: _7 = _1"
+            "bb1[2]: _7 = _1"
           ],
           "_8": [
-            "bb2[1]: _8 = _1"
+            "bb2[2]: _8 = _1"
           ],
           "_9": [
-            "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+            "bb2[3]: _9 = Eq(_8, const i32::MIN)"
           ]
         },
         "statement: StorageDead(_3)"
@@ -643,11 +658,11 @@ Result for function abs():
         "arg0"
       ],
       "_3": [
-        "bb1[2]: _3 = move _7",
+        "bb1[3]: _3 = move _7",
         "bb3[0]: _3 = Neg(move _8)"
       ],
       "_4": [
-        "bb1[4]: _4 = const ()",
+        "bb1[5]: _4 = const ()",
         "bb3[2]: _4 = const ()"
       ],
       "_5": [
@@ -657,13 +672,13 @@ Result for function abs():
         "bb0[4]: _6 = _1"
       ],
       "_7": [
-        "bb1[1]: _7 = _1"
+        "bb1[2]: _7 = _1"
       ],
       "_8": [
-        "bb2[1]: _8 = _1"
+        "bb2[2]: _8 = _1"
       ],
       "_9": [
-        "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+        "bb2[3]: _9 = Eq(_8, const i32::MIN)"
       ]
     },
     "terminator: return",
@@ -683,10 +698,10 @@ Result for function abs():
         "bb0[4]: _6 = _1"
       ],
       "_8": [
-        "bb2[1]: _8 = _1"
+        "bb2[2]: _8 = _1"
       ],
       "_9": [
-        "bb2[2]: _9 = Eq(_8, const i32::MIN)"
+        "bb2[3]: _9 = Eq(_8, const i32::MIN)"
       ]
     },
     "terminator: resume",
diff --git a/rr_frontend/analysis/tests/test_cases/reaching_definitions/calls.rs b/rr_frontend/analysis/tests/test_cases/reaching_definitions/calls.rs
index 0c6e1153..a9dadb0c 100644
--- a/rr_frontend/analysis/tests/test_cases/reaching_definitions/calls.rs
+++ b/rr_frontend/analysis/tests/test_cases/reaching_definitions/calls.rs
@@ -9,4 +9,4 @@ fn main() {
 
 fn f(x: i32) -> i32 {
     return x;
-}
\ No newline at end of file
+}
diff --git a/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.rs b/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.rs
index 29875ea2..007a91d8 100644
--- a/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.rs
+++ b/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.rs
@@ -5,8 +5,7 @@ fn main() {
     x = input();
     if x > 2 {
         y = 5;
-    }
-    else {
+    } else {
         y = 7;
     }
     y = 25;
@@ -14,4 +13,4 @@ fn main() {
 
 fn input() -> i32 {
     return 42;
-}
\ No newline at end of file
+}
diff --git a/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout b/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout
index 0ff17948..83583644 100644
--- a/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout
+++ b/rr_frontend/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout
@@ -215,27 +215,6 @@ Result for function main():
           ]
         },
         "statement: _5 = Gt(move _6, const 2_i32)"
-      ],
-      [
-        "state:",
-        {
-          "_1": [
-            "bb1[0]: _1 = move _3"
-          ],
-          "_2": [
-            "bb0[4]: _2 = const 3_i32"
-          ],
-          "_3": [
-            "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
-          ],
-          "_5": [
-            "bb1[6]: _5 = Gt(move _6, const 2_i32)"
-          ],
-          "_6": [
-            "bb1[5]: _6 = _1"
-          ]
-        },
-        "statement: StorageDead(_6)"
       ]
     ],
     "state before terminator:",
@@ -256,7 +235,7 @@ Result for function main():
         "bb1[5]: _6 = _1"
       ]
     },
-    "terminator: switchInt(move _5) -> [false: bb3, otherwise: bb2]",
+    "terminator: switchInt(move _5) -> [0: bb3, otherwise: bb2]",
     {
       "bb2": [
         "state:",
@@ -302,6 +281,27 @@ Result for function main():
   ],
   "bb2": [
     [
+      [
+        "state:",
+        {
+          "_1": [
+            "bb1[0]: _1 = move _3"
+          ],
+          "_2": [
+            "bb0[4]: _2 = const 3_i32"
+          ],
+          "_3": [
+            "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
+          ],
+          "_5": [
+            "bb1[6]: _5 = Gt(move _6, const 2_i32)"
+          ],
+          "_6": [
+            "bb1[5]: _6 = _1"
+          ]
+        },
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         {
@@ -330,7 +330,7 @@ Result for function main():
             "bb1[0]: _1 = move _3"
           ],
           "_2": [
-            "bb2[0]: _2 = const 5_i32"
+            "bb2[1]: _2 = const 5_i32"
           ],
           "_3": [
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
@@ -351,13 +351,13 @@ Result for function main():
         "bb1[0]: _1 = move _3"
       ],
       "_2": [
-        "bb2[0]: _2 = const 5_i32"
+        "bb2[1]: _2 = const 5_i32"
       ],
       "_3": [
         "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
       ],
       "_4": [
-        "bb2[1]: _4 = const ()"
+        "bb2[2]: _4 = const ()"
       ],
       "_5": [
         "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -375,13 +375,13 @@ Result for function main():
             "bb1[0]: _1 = move _3"
           ],
           "_2": [
-            "bb2[0]: _2 = const 5_i32"
+            "bb2[1]: _2 = const 5_i32"
           ],
           "_3": [
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb2[1]: _4 = const ()"
+            "bb2[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -395,6 +395,27 @@ Result for function main():
   ],
   "bb3": [
     [
+      [
+        "state:",
+        {
+          "_1": [
+            "bb1[0]: _1 = move _3"
+          ],
+          "_2": [
+            "bb0[4]: _2 = const 3_i32"
+          ],
+          "_3": [
+            "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
+          ],
+          "_5": [
+            "bb1[6]: _5 = Gt(move _6, const 2_i32)"
+          ],
+          "_6": [
+            "bb1[5]: _6 = _1"
+          ]
+        },
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         {
@@ -423,7 +444,7 @@ Result for function main():
             "bb1[0]: _1 = move _3"
           ],
           "_2": [
-            "bb3[0]: _2 = const 7_i32"
+            "bb3[1]: _2 = const 7_i32"
           ],
           "_3": [
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
@@ -444,13 +465,13 @@ Result for function main():
         "bb1[0]: _1 = move _3"
       ],
       "_2": [
-        "bb3[0]: _2 = const 7_i32"
+        "bb3[1]: _2 = const 7_i32"
       ],
       "_3": [
         "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
       ],
       "_4": [
-        "bb3[1]: _4 = const ()"
+        "bb3[2]: _4 = const ()"
       ],
       "_5": [
         "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -468,13 +489,13 @@ Result for function main():
             "bb1[0]: _1 = move _3"
           ],
           "_2": [
-            "bb3[0]: _2 = const 7_i32"
+            "bb3[1]: _2 = const 7_i32"
           ],
           "_3": [
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb3[1]: _4 = const ()"
+            "bb3[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -495,15 +516,15 @@ Result for function main():
             "bb1[0]: _1 = move _3"
           ],
           "_2": [
-            "bb2[0]: _2 = const 5_i32",
-            "bb3[0]: _2 = const 7_i32"
+            "bb2[1]: _2 = const 5_i32",
+            "bb3[1]: _2 = const 7_i32"
           ],
           "_3": [
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb2[1]: _4 = const ()",
-            "bb3[1]: _4 = const ()"
+            "bb2[2]: _4 = const ()",
+            "bb3[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -521,15 +542,15 @@ Result for function main():
             "bb1[0]: _1 = move _3"
           ],
           "_2": [
-            "bb2[0]: _2 = const 5_i32",
-            "bb3[0]: _2 = const 7_i32"
+            "bb2[1]: _2 = const 5_i32",
+            "bb3[1]: _2 = const 7_i32"
           ],
           "_3": [
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb2[1]: _4 = const ()",
-            "bb3[1]: _4 = const ()"
+            "bb2[2]: _4 = const ()",
+            "bb3[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -547,15 +568,15 @@ Result for function main():
             "bb1[0]: _1 = move _3"
           ],
           "_2": [
-            "bb2[0]: _2 = const 5_i32",
-            "bb3[0]: _2 = const 7_i32"
+            "bb2[1]: _2 = const 5_i32",
+            "bb3[1]: _2 = const 7_i32"
           ],
           "_3": [
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb2[1]: _4 = const ()",
-            "bb3[1]: _4 = const ()"
+            "bb2[2]: _4 = const ()",
+            "bb3[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -579,8 +600,8 @@ Result for function main():
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb2[1]: _4 = const ()",
-            "bb3[1]: _4 = const ()"
+            "bb2[2]: _4 = const ()",
+            "bb3[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -607,8 +628,8 @@ Result for function main():
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb2[1]: _4 = const ()",
-            "bb3[1]: _4 = const ()"
+            "bb2[2]: _4 = const ()",
+            "bb3[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -635,8 +656,8 @@ Result for function main():
             "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
           ],
           "_4": [
-            "bb2[1]: _4 = const ()",
-            "bb3[1]: _4 = const ()"
+            "bb2[2]: _4 = const ()",
+            "bb3[2]: _4 = const ()"
           ],
           "_5": [
             "bb1[6]: _5 = Gt(move _6, const 2_i32)"
@@ -663,8 +684,8 @@ Result for function main():
         "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]"
       ],
       "_4": [
-        "bb2[1]: _4 = const ()",
-        "bb3[1]: _4 = const ()"
+        "bb2[2]: _4 = const ()",
+        "bb3[2]: _4 = const ()"
       ],
       "_5": [
         "bb1[6]: _5 = Gt(move _6, const 2_i32)"
diff --git a/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.rs b/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.rs
index 7af149c9..e70e687a 100644
--- a/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.rs
+++ b/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.rs
@@ -1,8 +1,7 @@
-
 fn main() {
     let a = abs(-1);
     let b = abs(1);
-    println!("{}", a+b);
+    println!("{}", a + b);
 }
 
 #[analyzer::run]
@@ -10,8 +9,7 @@ fn abs(x: i32) -> i32 {
     let res: i32;
     if x >= 0 {
         res = x;
-    }
-    else {
+    } else {
         res = -x;
     }
     return res;
diff --git a/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout b/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout
index 6b0ca3a6..3aee1e2d 100644
--- a/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout
+++ b/rr_frontend/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout
@@ -45,42 +45,45 @@ Result for function abs():
           "_6"
         ],
         "statement: _5 = Ge(move _6, const 0_i32)"
-      ],
-      [
-        "state:",
-        [
-          "_1",
-          "_5",
-          "_6"
-        ],
-        "statement: StorageDead(_6)"
       ]
     ],
     "state before terminator:",
     [
       "_1",
-      "_5"
+      "_5",
+      "_6"
     ],
-    "terminator: switchInt(move _5) -> [false: bb2, otherwise: bb1]",
+    "terminator: switchInt(move _5) -> [0: bb2, otherwise: bb1]",
     {
       "bb1": [
         "state:",
         [
           "_1",
-          "_5"
+          "_5",
+          "_6"
         ]
       ],
       "bb2": [
         "state:",
         [
           "_1",
-          "_5"
+          "_5",
+          "_6"
         ]
       ]
     }
   ],
   "bb1": [
     [
+      [
+        "state:",
+        [
+          "_1",
+          "_5",
+          "_6"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
@@ -148,6 +151,15 @@ Result for function abs():
   ],
   "bb2": [
     [
+      [
+        "state:",
+        [
+          "_1",
+          "_5",
+          "_6"
+        ],
+        "statement: StorageDead(_6)"
+      ],
       [
         "state:",
         [
-- 
GitLab