From 58a47cd03ffa1ad5bf378f0074f6e35018bc09c2 Mon Sep 17 00:00:00 2001
From: Alexa VanHattum <alexavanhattum@gmail.com>
Date: Wed, 21 Jul 2021 10:02:53 -0400
Subject: [PATCH] Fix dyn trait _fail tests compilation errors (#342)

---
 src/test/cbmc/DynTrait/main_fail.rs         |  4 ++--
 src/test/cbmc/DynTrait/nested_boxes_fail.rs | 11 +++++++----
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/src/test/cbmc/DynTrait/main_fail.rs b/src/test/cbmc/DynTrait/main_fail.rs
index 0c51a3b408d37..045832ba9b057 100644
--- a/src/test/cbmc/DynTrait/main_fail.rs
+++ b/src/test/cbmc/DynTrait/main_fail.rs
@@ -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");
     }
 }
diff --git a/src/test/cbmc/DynTrait/nested_boxes_fail.rs b/src/test/cbmc/DynTrait/nested_boxes_fail.rs
index 8327a16c5f71c..d3001ddb8053d 100644
--- a/src/test/cbmc/DynTrait/nested_boxes_fail.rs
+++ b/src/test/cbmc/DynTrait/nested_boxes_fail.rs
@@ -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");
 
@@ -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);
@@ -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>());