Skip to content

Commit

Permalink
Fix dyn trait _fail tests compilation errors (rust-lang#342)
Browse files Browse the repository at this point in the history
  • Loading branch information
avanhatt authored and tedinski committed Jul 21, 2021
1 parent c39c268 commit 58a47cd
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 6 deletions.
4 changes: 2 additions & 2 deletions src/test/cbmc/DynTrait/main_fail.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ fn main() {
let animal = random_animal(random_number);
let s = animal.noise();
if (random_number < 5) {
_VERIFIER_expect_fail(s == 2, "Wrong noise");
__VERIFIER_expect_fail(s == 2, "Wrong noise");
} else {
_VERIFIER_expect_fail(s == 1, "Wrong noise");
__VERIFIER_expect_fail(s == 1, "Wrong noise");
}
}
11 changes: 7 additions & 4 deletions src/test/cbmc/DynTrait/nested_boxes_fail.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,9 @@
#![feature(core_intrinsics)]
#![feature(ptr_metadata)]

use std::any::Any;
use std::intrinsics::size_of;
use std::ptr::DynMetadata;

include!("../Helpers/vtable_utils_ignore.rs");

Expand All @@ -26,15 +28,16 @@ fn main() {
unsafe {
// Outermost trait object
// The size is 16, because the data is another fat pointer
let vtable3: *mut usize = vtable!(dyn_trait3);
let dyn_3 = &*dyn_trait3 as &dyn Send;
let vtable3: DynMetadata<dyn Any> = vtable!(dyn_3);
assert!(size_from_vtable(vtable3) != 16);
assert!(align_from_vtable(vtable3) != 8);

// Inspect the data pointer from dyn_trait3
let data_ptr3 = data!(dyn_trait3) as *mut usize;
let data_ptr3 = data!(dyn_3) as *mut usize;

// The second half of this fat pointer is another vtable, for dyn_trait2
let vtable2 = *(data_ptr3.offset(1) as *mut *mut usize);
let vtable2 = *(data_ptr3.offset(1) as *mut DynMetadata<dyn Any>);

// The size is 16, because the data is another fat pointer
assert!(size_from_vtable(vtable2) != 16);
Expand All @@ -44,7 +47,7 @@ fn main() {
let data_ptr2 = *(data_ptr3 as *mut *mut usize);

// The second half of this fat pointer is another vtable, for dyn_trait1
let vtable1 = *(data_ptr2.offset(1) as *mut *mut usize);
let vtable1 = *(data_ptr2.offset(1) as *mut DynMetadata<dyn Any>);

// The size is 8, because the data is the Foo itself
assert!(size_from_vtable(vtable1) != size_of::<Foo>());
Expand Down

0 comments on commit 58a47cd

Please sign in to comment.