From a1dccb2c3454ed9857b6b1bc24eb10841e8b0722 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Fri, 28 Jun 2024 14:01:50 -0700 Subject: [PATCH] Throw an error only if the unsize cast happens to a pointer to trait object --- .../transform/check_uninit/uninit_visitor.rs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs index 551bc660c78b..950cd66203c5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs @@ -520,10 +520,14 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } fn visit_rvalue(&mut self, rvalue: &Rvalue, location: Location) { - if let Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), _, _) = rvalue { - self.push_target(MemoryInitOp::Unsupported { - reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), - }); + if let Rvalue::Cast(CastKind::PointerCoercion(PointerCoercion::Unsize), _, ty) = rvalue { + if let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ty.kind() { + if pointee_ty.kind().is_trait() { + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization of unsized pointers.".to_string(), + }); + } + } }; self.super_rvalue(rvalue, location); }