Better unsupported construct messages (rust-lang#1725)

celinval · Sep 28, 2022 · d86dc3b · d86dc3b
1 parent 21ceaa2
commit d86dc3b
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 5 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -836,7 +836,7 @@ impl<'tcx> GotocCtx<'tcx> {
             let drop_sym = self.ensure(&drop_sym_name, |ctx, name| {
                 // Function body
                 let unimplemented = ctx.codegen_unimplemented_stmt(
-                    format!("drop_in_place for {}", drop_sym_name).as_str(),
+                    format!("drop_in_place for {}", drop_instance).as_str(),
                     Location::none(),
                     "https://github.com/model-checking/kani/issues/281",
                 );

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -334,7 +334,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             if !(typ.is_trait() || typ.is_box()) {
                                 warn!(self_type=?typ, "Unsupported drop of unsized");
                                 return self.codegen_unimplemented_stmt(
-                                    format!("Unsupported drop unsized struct: {:?}", typ).as_str(),
+                                    format!("drop unsized struct for {:?}", typ).as_str(),
                                     loc,
                                     "https://github.com/model-checking/kani/issues/1072",
                                 );
@@ -383,7 +383,11 @@ impl<'tcx> GotocCtx<'tcx> {
                             func.call(args).as_stmt(loc)
                         } else {
                             self.codegen_unimplemented_stmt(
-                                format!("drop_in_place call for {:?}", func).as_str(),
+                                format!(
+                                    "drop_in_place call for {}",
+                                    self.readable_instance_name(drop_instance)
+                                )
+                                .as_str(),
                                 loc,
                                 "https://github.com/model-checking/kani/issues/426",
                             )

diff --git a/tests/expected/drop/expected b/tests/expected/drop/expected
@@ -7,10 +7,10 @@ Description: "assertion failed: self.id == 1"\
 in function <DummyImpl as std::ops::Drop>::drop
 
 Status: FAILURE\
-Description: "Unsupported drop unsized struct: Wrapper<dyn DummyTrait> is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/1072"
+Description: "drop unsized struct for Wrapper<dyn DummyTrait> is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/1072"
 
 
-Failed Checks: Unsupported drop unsized struct: Wrapper<dyn DummyTrait> is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/1072
+Failed Checks: drop unsized struct for Wrapper<dyn DummyTrait> is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/1072
 
 VERIFICATION:- FAILED