Skip to content

Bad pointer deref in SizeAndAlignOfDst/main_fail.rs #87

@markrtuttle

Description

@markrtuttle

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.

Type

No type

Projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions