-
Notifications
You must be signed in to change notification settings - Fork 126
Closed
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.
Milestone
Description
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.
Metadata
Metadata
Assignees
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.