RMC fails to cast a "mutable raw pointer to a trait object" to a "mutable raw pointer to a unit" that arises in the regression test rust-tests/cbmc-reg/SizeAndAlignOfDst/main_fail.rs described in issue #33 that was used initially to illustrate an issue with the unsized pointer cast.
The mir generated by rustc on the test includes
handling rc::is_dangling::<alloc::sync::ArcInner<Mutex<dyn Subscriber>>>, std::rc::is_dangling
let _1: *mut alloc::sync::ArcInner<std::sync::Mutex<dyn Subscriber>>
let _3: *mut ()
let _4: *mut alloc::sync::ArcInner<std::sync::Mutex<dyn Subscriber>>
_4 = _1
_3 = move _4 as *mut () (Misc)
where you can see that the pointer to the trait object (a fat pointer) is being cast to a pointer to a unit (thin pointer), and codegen_misc_cast fails because the cast_to predicate says you can't cast a goto struct to a goto pointer.
RMC fails to cast a "mutable raw pointer to a trait object" to a "mutable raw pointer to a unit" that arises in the regression test
rust-tests/cbmc-reg/SizeAndAlignOfDst/main_fail.rsdescribed in issue #33 that was used initially to illustrate an issue with the unsized pointer cast.The mir generated by rustc on the test includes
where you can see that the pointer to the trait object (a fat pointer) is being cast to a pointer to a unit (thin pointer), and
codegen_misc_castfails because thecast_topredicate says you can't cast a goto struct to a goto pointer.