Gracefully error on stolen bodies

charon/src/bin/charon-driver/translate/get_mir.rs

@@ -40,11 +40,17 @@ pub fn get_mir_for_def_id_and_level(
         match level {
             MirLevel::Built => {
                 let body = tcx.mir_built(local_def_id);
+                if body.is_stolen() {
+                    return None;
+                }
                 // We clone to be sure there are no problems with locked values
                 body.borrow().clone()
             }
             MirLevel::Promoted => {
                 let (body, _) = tcx.mir_promoted(local_def_id);
+                if body.is_stolen() {
+                    return None;
+                }
                 // We clone to be sure there are no problems with locked values
                 body.borrow().clone()
             }

charon/tests/ui/stealing.out

@@ -0,0 +1,16 @@
+# Final LLBC before serialization:
+
+global test_crate::SLICE  {
+    let @0: Array<(), 4 : usize>; // return
+    let @1: (); // anonymous local
+
+    @1 := ()
+    @0 := @ArrayRepeat<'_, (), 4 : usize>(move (@1))
+    drop @1
+    return
+}
+
+fn test_crate::four() -> usize
+
+
+

charon/tests/ui/stealing.rs

@@ -0,0 +1,7 @@
+// Translating this needs the evaluatable MIR of `fn four()`, which steals its `mir_built` body.
+// There's no simple ordering of the translation of items that can avoid all stealing.
+static SLICE: [(); four()] = [(); 4];
+
+const fn four() -> usize {
+    2 + 2
+}