From f860d198b7746514cf34ea2483dca5572947c1f4 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Mon, 21 Jun 2021 07:50:57 -0400 Subject: [PATCH 1/3] Add vtable drop_in_place --- .../rustc_codegen_llvm/src/gotoc/rvalue.rs | 39 +++++++++---------- .../rustc_codegen_llvm/src/gotoc/statement.rs | 1 + compiler/rustc_codegen_llvm/src/gotoc/typ.rs | 11 +++--- ...ize_align.rs => vtable_size_align_drop.rs} | 5 ++- ...fail.rs => vtable_size_align_drop_fail.rs} | 4 +- src/test/cbmc/Helpers/vtable_utils_ignore.rs | 7 ++++ 6 files changed, 37 insertions(+), 30 deletions(-) rename src/test/cbmc/DynTrait/{vtable_size_align.rs => vtable_size_align_drop.rs} (94%) rename src/test/cbmc/DynTrait/{vtable_size_align_fail.rs => vtable_size_align_drop_fail.rs} (95%) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 8eb60a541de5..eed226cc42c2 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -712,26 +712,23 @@ impl<'tcx> GotocCtx<'tcx> { } } - fn codegen_vtable_drop_in_place(&self) -> Expr { - // TODO: The following still needs to be done for the destructor (drop_in_place method), but before that - // the right type for drop_in_place needs to be set in typ.rs in codegen_ty_ref method as well. - // Atm we pass a nullpointer instead (Type::empty().pointer(ctx.ptr_width()).null() in vtable_base) - // This is sound, because CBMC will give a pointer error if we ever actually use it. - // - // let drop_instance = - // Instance::resolve_drop_in_place(ctx.tcx, operand_type); - // let drop_method_name = self.symbol_name(drop_instance); - // let drop_inst_type = - // drop_instance.ty(self.tcx, ty::ParamEnv::reveal_all()); - // let drop_irep = data::Variable { - // data: drop_method_name.clone(), - // typ: self.codegen_ty(drop_inst_type), - // // typ: output_type, - // location: data::Irep::nil(), - // } - // .to_expr() - // .address_of(); - Type::void_pointer().null() + /// Generate a function pointer to drop_in_place for entry into the vtable + fn codegen_vtable_drop_in_place( + &mut self, + ty: Ty<'tcx>, + trait_ty: &'tcx ty::TyS<'tcx>, + ) -> Expr { + let drop_instance = Instance::resolve_drop_in_place(self.tcx, ty); + let drop_sym_name = self.symbol_name(drop_instance); + let drop_sym = self.symbol_table.lookup(&drop_sym_name).unwrap().clone(); + + // The drop instance has the concrete object type, for consistency with + // type codegen we need the trait type for the function parameter. + let trait_fn_ty = + Type::code_with_unnamed_parameters(vec![self.codegen_ty(trait_ty)], Type::unit()) + .to_pointer(); + + Expr::symbol_expression(drop_sym_name, drop_sym.typ).address_of().cast_to(trait_fn_ty) } fn codegen_vtable_methods( @@ -825,7 +822,7 @@ impl<'tcx> GotocCtx<'tcx> { |ctx, var| { // Build the vtable // See compiler/rustc_codegen_llvm/src/gotoc/typ.rs `trait_vtable_field_types` for field order - let drop_irep = ctx.codegen_vtable_drop_in_place(); + let drop_irep = ctx.codegen_vtable_drop_in_place(&src_mir_type, trait_type); let (vt_size, vt_align) = ctx.codegen_vtable_size_and_align(&src_mir_type); let size_assert = ctx.check_vtable_size(&src_mir_type, vt_size.clone()); let mut vtable_fields = vec![drop_irep, vt_size, vt_align]; diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index 43f52886f2cb..57e5698c4ed9 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -96,6 +96,7 @@ impl<'tcx> GotocCtx<'tcx> { } // TODO: this function doesn't handle unwinding which begins if the destructor panics + // https://github.com/model-checking/rmc/issues/221 fn codegen_drop(&mut self, location: &Place<'tcx>, target: &BasicBlock) -> Stmt { // instance for drop function let loc_ty = self.place_ty(location); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index ca1634134450..5aab106d6120 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs @@ -175,13 +175,14 @@ impl<'tcx> GotocCtx<'tcx> { /// The order of fields (i.e., the layout of a vtable) is not guaranteed by the compiler. /// We follow the order implemented by the compiler in compiler/rustc_codegen_ssa/src/meth.rs /// `get_vtable`. - /// - /// Currently, we also add a well-formed flag field to the end of the struct. fn trait_vtable_field_types(&mut self, t: &'tcx ty::TyS<'tcx>) -> Vec { + // `drop_in_place` is a function with type t -> (), the vtable needs a + // pointer to it + let drop_ty = + Type::code_with_unnamed_parameters(vec![self.codegen_ty(t)], Type::unit()).to_pointer(); + let mut vtable_base = vec![ - // TODO: get the correct type for the drop in place. For now, just use void* - // https://github.com/model-checking/rmc/issues/11 - Type::datatype_component("drop", Type::void_pointer()), + Type::datatype_component("drop", drop_ty), Type::datatype_component("size", Type::size_t()), Type::datatype_component("align", Type::size_t()), ]; diff --git a/src/test/cbmc/DynTrait/vtable_size_align.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs similarity index 94% rename from src/test/cbmc/DynTrait/vtable_size_align.rs rename to src/test/cbmc/DynTrait/vtable_size_align_drop.rs index 58a5db683c19..c6d546c10e88 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs @@ -12,6 +12,7 @@ use std::intrinsics::size_of; use std::mem::transmute; +use std::ptr::drop_in_place; use std::raw::TraitObject; include!("../Helpers/vtable_utils_ignore.rs"); @@ -85,7 +86,7 @@ fn main() { let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(!vtable_ptr.is_null()); + assert!(drop_from_vtrable(vtable_ptr) == drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); @@ -107,7 +108,7 @@ fn main() { let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(!vtable_ptr.is_null()); + assert!(drop_from_vtrable(vtable_ptr) == drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); diff --git a/src/test/cbmc/DynTrait/vtable_size_align_fail.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs similarity index 95% rename from src/test/cbmc/DynTrait/vtable_size_align_fail.rs rename to src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs index 267ed54e304d..2a4f4c1b4014 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_fail.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs @@ -87,7 +87,7 @@ fn main() { let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(vtable_ptr.is_null()); + assert!(drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) != size_of::()); @@ -109,7 +109,7 @@ fn main() { let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer - assert!(vtable_ptr.is_null()); + assert!(drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut ()); // Size and align as usizes assert!(size_from_vtable(vtable_ptr) != size_of::()); diff --git a/src/test/cbmc/Helpers/vtable_utils_ignore.rs b/src/test/cbmc/Helpers/vtable_utils_ignore.rs index b7d843947a9e..c4b0e36b8a8f 100644 --- a/src/test/cbmc/Helpers/vtable_utils_ignore.rs +++ b/src/test/cbmc/Helpers/vtable_utils_ignore.rs @@ -3,6 +3,13 @@ // Because each regression test does not share a crate, we just use // an import! to share this code across test directories. +fn drop_from_vtrable(vtable_ptr : *mut usize) -> *mut () { + // 2nd usize-sized position + unsafe { + *vtable_ptr as *mut () + } +} + fn size_from_vtable(vtable_ptr : *mut usize) -> usize { // 2nd usize-sized position unsafe { From 8e76af3369208558c3ca4970253d3a554550e00e Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Mon, 21 Jun 2021 11:28:41 -0400 Subject: [PATCH 2/3] DSN comments --- .../cbmc/DynTrait/vtable_size_align_drop.rs | 33 +++-- .../DynTrait/vtable_size_align_drop_fail.rs | 119 ------------------ src/test/cbmc/Helpers/vtable_utils_ignore.rs | 2 +- 3 files changed, 22 insertions(+), 132 deletions(-) delete mode 100644 src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs index c6d546c10e88..87a66dd92feb 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs @@ -1,7 +1,7 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// This test checks the `size` and `align` fields of vtables, for a +// This test checks the `size` and `align` fields of vtables, for a // dynamic trait where two implementing structs have different sizes. // The strategy is to cast the dyn trait object to a raw::TraitObject // then do some unsafe pointer math. @@ -46,10 +46,10 @@ impl Animal for Cow { // Returns some struct that implements Animal, but we don't know which one at compile time. fn random_animal(random_number: i64) -> Box { - if random_number < 5 { - Box::new(Sheep { sheep_num : 7 }) - } else { - Box::new(Cow { cow_num : 9 }) + if random_number < 5 { + Box::new(Sheep { sheep_num: 7 }) + } else { + Box::new(Cow { cow_num: 9 }) } } @@ -57,7 +57,7 @@ fn main() { let ptr_size = size_of::<&usize>() as isize; // The vtable is laid out as the right hand side here: - // + // // +-------+------------------+ // | size | value | // +-------+------------------+ @@ -66,8 +66,8 @@ fn main() { // | usize | align in bytes | // | ? | function ptrs... | // +-------+------------------+ - // - // This layout taken from miri's handling: + // + // This layout taken from miri's handling: // https://github.com/rust-lang/rust/blob/ec487bf3cfc9ce386da25169509fae8f2b4d4eec/compiler/rustc_mir/src/interpret/traits.rs#L155 // Check layout/values for Sheep @@ -82,7 +82,7 @@ fn main() { // Note: i32 ptr cast assert!(*(data_ptr as *mut i32) == 7); // From Sheep - + let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer @@ -91,8 +91,13 @@ fn main() { // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); assert!(align_from_vtable(vtable_ptr) == size_of::()); + + // Expect failures + __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 7, "wrong data"); + __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::()); + __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::()); } - // Check layout/values for Cow + // Check layout/values for Cow unsafe { let animal_cow = random_animal(6); @@ -104,7 +109,7 @@ fn main() { // Note: i8 ptr cast assert!(*(data_ptr as *mut i8) == 9); // From Cow - + let vtable_ptr = trait_object.vtable as *mut usize; // Drop pointer @@ -113,6 +118,10 @@ fn main() { // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); assert!(align_from_vtable(vtable_ptr) == size_of::()); + + // Expect failures + __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 9, "wrong data"); + __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::()); + __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::()); } } - \ No newline at end of file diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs deleted file mode 100644 index 2a4f4c1b4014..000000000000 --- a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs +++ /dev/null @@ -1,119 +0,0 @@ -// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. -// SPDX-License-Identifier: Apache-2.0 OR MIT - -// This test checks the `size` and `align` fields of vtables, for a -// dynamic trait where two implementing structs have different sizes. -// The strategy is to cast the dyn trait object to a raw::TraitObject -// then do some unsafe pointer math. - -// In this _fail version, all asserts should fail. - -#![feature(core_intrinsics)] -#![feature(raw)] -#![allow(deprecated)] - -use std::intrinsics::size_of; -use std::mem::transmute; -use std::raw::TraitObject; - -include!("../Helpers/vtable_utils_ignore.rs"); - -// Different sized data fields on each struct -struct Sheep { - pub sheep_num: i32, -} -struct Cow { - pub cow_num: i8, -} - -trait Animal { - // Instance method signature - fn noise(&self) -> i32; -} - -// Implement the `Animal` trait for `Sheep`. -impl Animal for Sheep { - fn noise(&self) -> i32 { - self.sheep_num - } -} - -// Implement the `Animal` trait for `Cow`. -impl Animal for Cow { - fn noise(&self) -> i32 { - self.cow_num as i32 - } -} - -// Returns some struct that implements Animal, but we don't know which one at compile time. -fn random_animal(random_number: i64) -> Box { - if random_number < 5 { - Box::new(Sheep { sheep_num : 7 }) - } else { - Box::new(Cow { cow_num : 9 }) - } -} - -fn main() { - let ptr_size = size_of::<&usize>() as isize; - - // The vtable is laid out as the right hand side here: - // - // +-------+------------------+ - // | size | value | - // +-------+------------------+ - // | usize | pointer to drop | - // | usize | size in bytes | - // | usize | align in bytes | - // | ? | function ptrs... | - // +-------+------------------+ - // - // This layout taken from miri's handling: - // https://github.com/rust-lang/rust/blob/ec487bf3cfc9ce386da25169509fae8f2b4d4eec/compiler/rustc_mir/src/interpret/traits.rs#L155 - - // Check layout/values for Sheep - unsafe { - let animal_sheep = random_animal(1); - - // Unsafe cast to dynamic trait object fat pointer - let trait_object: TraitObject = transmute(animal_sheep); - - // Check that the struct's data is what we expect - let data_ptr = trait_object.data; - - // Note: i32 ptr cast - assert!(*(data_ptr as *mut i32) != 7); // From Sheep - - let vtable_ptr = trait_object.vtable as *mut usize; - - // Drop pointer - assert!(drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut ()); - - // Size and align as usizes - assert!(size_from_vtable(vtable_ptr) != size_of::()); - assert!(align_from_vtable(vtable_ptr) != size_of::()); - } - // Check layout/values for Cow - unsafe { - let animal_cow = random_animal(6); - - // Unsafe cast to dynamic trait object fat pointer - let trait_object: TraitObject = transmute(animal_cow); - - // Check that the struct's data is what we expect - let data_ptr = trait_object.data; - - // Note: i8 ptr cast - assert!(*(data_ptr as *mut i8) != 9); // From Cow - - let vtable_ptr = trait_object.vtable as *mut usize; - - // Drop pointer - assert!(drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut ()); - - // Size and align as usizes - assert!(size_from_vtable(vtable_ptr) != size_of::()); - assert!(align_from_vtable(vtable_ptr) != size_of::()); - } -} - \ No newline at end of file diff --git a/src/test/cbmc/Helpers/vtable_utils_ignore.rs b/src/test/cbmc/Helpers/vtable_utils_ignore.rs index c4b0e36b8a8f..74c60d5305c2 100644 --- a/src/test/cbmc/Helpers/vtable_utils_ignore.rs +++ b/src/test/cbmc/Helpers/vtable_utils_ignore.rs @@ -4,7 +4,7 @@ // Because each regression test does not share a crate, we just use // an import! to share this code across test directories. fn drop_from_vtrable(vtable_ptr : *mut usize) -> *mut () { - // 2nd usize-sized position + // 1st pointer-sized position unsafe { *vtable_ptr as *mut () } From 87ff2da96a7f2dae78407b4fceea09889d1c8065 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Mon, 21 Jun 2021 12:57:16 -0400 Subject: [PATCH 3/3] Fix __VERIFIER_expect_fail --- .../cbmc/DynTrait/vtable_size_align_drop.rs | 12 -- .../DynTrait/vtable_size_align_drop_fail.rs | 126 ++++++++++++++++++ src/test/rmc-prelude.rs | 2 +- 3 files changed, 127 insertions(+), 13 deletions(-) create mode 100644 src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs index 87a66dd92feb..48d576fd0be5 100644 --- a/src/test/cbmc/DynTrait/vtable_size_align_drop.rs +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop.rs @@ -54,8 +54,6 @@ fn random_animal(random_number: i64) -> Box { } fn main() { - let ptr_size = size_of::<&usize>() as isize; - // The vtable is laid out as the right hand side here: // // +-------+------------------+ @@ -91,11 +89,6 @@ fn main() { // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); assert!(align_from_vtable(vtable_ptr) == size_of::()); - - // Expect failures - __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 7, "wrong data"); - __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::()); - __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::()); } // Check layout/values for Cow unsafe { @@ -118,10 +111,5 @@ fn main() { // Size and align as usizes assert!(size_from_vtable(vtable_ptr) == size_of::()); assert!(align_from_vtable(vtable_ptr) == size_of::()); - - // Expect failures - __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 9, "wrong data"); - __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::()); - __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::()); } } diff --git a/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs new file mode 100644 index 000000000000..126e5e0a135d --- /dev/null +++ b/src/test/cbmc/DynTrait/vtable_size_align_drop_fail.rs @@ -0,0 +1,126 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks the `size` and `align` fields of vtables, for a +// dynamic trait where two implementing structs have different sizes. +// The strategy is to cast the dyn trait object to a raw::TraitObject +// then do some unsafe pointer math. + +// In this _fail version, all asserts should fail. + +#![feature(core_intrinsics)] +#![feature(raw)] +#![allow(deprecated)] + +use std::intrinsics::size_of; +use std::mem::transmute; +use std::ptr::drop_in_place; +use std::raw::TraitObject; + +include!("../Helpers/vtable_utils_ignore.rs"); +include!("../../rmc-prelude.rs"); + +// Different sized data fields on each struct +struct Sheep { + pub sheep_num: i32, +} +struct Cow { + pub cow_num: i8, +} + +trait Animal { + // Instance method signature + fn noise(&self) -> i32; +} + +// Implement the `Animal` trait for `Sheep`. +impl Animal for Sheep { + fn noise(&self) -> i32 { + self.sheep_num + } +} + +// Implement the `Animal` trait for `Cow`. +impl Animal for Cow { + fn noise(&self) -> i32 { + self.cow_num as i32 + } +} + +// Returns some struct that implements Animal, but we don't know which one at compile time. +fn random_animal(random_number: i64) -> Box { + if random_number < 5 { + Box::new(Sheep { sheep_num: 7 }) + } else { + Box::new(Cow { cow_num: 9 }) + } +} + +fn main() { + let ptr_size = size_of::<&usize>() as isize; + + // The vtable is laid out as the right hand side here: + // + // +-------+------------------+ + // | size | value | + // +-------+------------------+ + // | usize | pointer to drop | + // | usize | size in bytes | + // | usize | align in bytes | + // | ? | function ptrs... | + // +-------+------------------+ + // + // This layout taken from miri's handling: + // https://github.com/rust-lang/rust/blob/ec487bf3cfc9ce386da25169509fae8f2b4d4eec/compiler/rustc_mir/src/interpret/traits.rs#L155 + + // Check layout/values for Sheep + unsafe { + let animal_sheep = random_animal(1); + + // Unsafe cast to dynamic trait object fat pointer + let trait_object: TraitObject = transmute(animal_sheep); + + // Check that the struct's data is what we expect + let data_ptr = trait_object.data; + + // Note: i32 ptr cast + __VERIFIER_expect_fail(*(data_ptr as *mut i32) != 7, "Wrong data"); // From Sheep + + let vtable_ptr = trait_object.vtable as *mut usize; + + // Drop pointer + __VERIFIER_expect_fail( + drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut (), + "Wrong drop", + ); + + // Size and align as usizes + __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); + __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); + } + // Check layout/values for Cow + unsafe { + let animal_cow = random_animal(6); + + // Unsafe cast to dynamic trait object fat pointer + let trait_object: TraitObject = transmute(animal_cow); + + // Check that the struct's data is what we expect + let data_ptr = trait_object.data; + + // Note: i8 ptr cast + __VERIFIER_expect_fail(*(data_ptr as *mut i8) != 9, "Wrong data"); // From Cow + + let vtable_ptr = trait_object.vtable as *mut usize; + + // Drop pointer + __VERIFIER_expect_fail( + drop_from_vtrable(vtable_ptr) != drop_in_place:: as *mut (), + "Wrong drop", + ); + + // Size and align as usizes + __VERIFIER_expect_fail(size_from_vtable(vtable_ptr) != size_of::(), "Wrong size"); + __VERIFIER_expect_fail(align_from_vtable(vtable_ptr) != size_of::(), "Wrong align"); + } +} diff --git a/src/test/rmc-prelude.rs b/src/test/rmc-prelude.rs index 05ce76d90d1a..32949166a1f9 100644 --- a/src/test/rmc-prelude.rs +++ b/src/test/rmc-prelude.rs @@ -5,7 +5,7 @@ fn __VERIFIER_assume(cond: bool) { unimplemented!() } -fn __VERIFIER_expect_fail(cond: bool) { +fn __VERIFIER_expect_fail(cond: bool, message: &str) { unimplemented!() }