Skip to content

Commit fbd5264

Browse files
authored
Declare unreachable intrinsic as unreachable (rust-lang#1119)
1 parent 6ffdbc2 commit fbd5264

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -609,6 +609,9 @@ impl<'tcx> GotocCtx<'tcx> {
609609
}
610610
"unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow),
611611
"unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)),
612+
"unreachable" => unreachable!(
613+
"Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
614+
),
612615
"volatile_copy_memory" => unstable_codegen!(codegen_intrinsic_copy!(Memmove)),
613616
"volatile_copy_nonoverlapping_memory" => {
614617
unstable_codegen!(codegen_intrinsic_copy!(Memcpy))

0 commit comments

Comments
 (0)