Skip to content

Commit 83c7fc5

Browse files
celinvaltedinski
authored andcommitted
Change how we fail when finding ThreadLocalInfo
Instead of crashing, we now will generate an assert(false) / assume(false) in the place of the ThreadLocalInfo expression.
1 parent 4643e33 commit 83c7fc5

File tree

1 file changed

+9
-1
lines changed
  • compiler/rustc_codegen_rmc/src/codegen

1 file changed

+9
-1
lines changed

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -430,7 +430,15 @@ impl<'tcx> GotocCtx<'tcx> {
430430
Rvalue::Aggregate(ref k, operands) => {
431431
self.codegen_rvalue_aggregate(&*k, operands, res_ty)
432432
}
433-
Rvalue::ThreadLocalRef(_) => unimplemented!(),
433+
Rvalue::ThreadLocalRef(_) => {
434+
let typ = self.codegen_ty(res_ty);
435+
self.codegen_unimplemented(
436+
"Rvalue::ThreadLocalRef",
437+
typ,
438+
Location::none(),
439+
"https://github.com/model-checking/rmc/issues/541",
440+
)
441+
}
434442
}
435443
}
436444

0 commit comments

Comments
 (0)