Skip to content

Commit

Permalink
Add UnsafeBinder variant (WIP in rustc).
Browse files Browse the repository at this point in the history
Rustc has started implementing `UnsafeBinder`:
- rust-lang/rust#134625
- rust-lang/rust#130516
Only the enums variants have been added for now, semantics is TBD.
  • Loading branch information
Remi Delmas committed Jan 7, 2025
1 parent feca7ab commit 75ce5d6
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -625,6 +625,8 @@ impl<'tcx> GotocCtx<'tcx> {
ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => {
unreachable!("remnants of type checking")
}
// TODO cf. https://github.com/rust-lang/rust/issues/130516
ty::UnsafeBinder(_) => todo!(),
}
}

Expand Down Expand Up @@ -1032,6 +1034,8 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()),
// TODO cf. https://github.com/rust-lang/rust/issues/130516
ty::UnsafeBinder(_) => todo!(),
}
}

Expand Down

0 comments on commit 75ce5d6

Please sign in to comment.