Closed
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.
Activity
avanhatt commentedon Jun 28, 2021
The cast now succeeds; but the test itself fails with a verification failure. Not sure if this is expected behavior because CBMC can't reason about locks. Will confirm and close issue if expected. Code in question:
avanhatt commentedon Jul 7, 2021
The test does also fail with invalid references when you pass
--pointer-check
, likely related to #240. Keeping open.Merge pull request #87 from rust-lang/feat/sat-abs-neg
31 remaining items