Skip to content

Commit

Permalink
Throw an error only if the unsize cast happens to a pointer to trait …
Browse files Browse the repository at this point in the history
…object
  • Loading branch information
artemagvanian committed Jun 28, 2024
1 parent f266ea9 commit a1dccb2
Showing 1 changed file with 8 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down

0 comments on commit a1dccb2

Please sign in to comment.