From 60572fcbffadd0cdfbec62dd05decb6ec0252e15 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 10 Jun 2024 20:49:08 +0000
Subject: [PATCH] Expand test

---
 tests/kani/FatPointers/metadata.rs | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/tests/kani/FatPointers/metadata.rs b/tests/kani/FatPointers/metadata.rs
index 0f3236f4c8a2..f76798e0f9f4 100644
--- a/tests/kani/FatPointers/metadata.rs
+++ b/tests/kani/FatPointers/metadata.rs
@@ -3,7 +3,22 @@
 
 #![feature(ptr_metadata)]
 
+struct S {
+    x: i32,
+}
+
+trait T {}
+
+impl T for S {}
+
 #[kani::proof]
 fn ptr_metadata() {
     assert_eq!(std::ptr::metadata("foo"), 3_usize);
+
+    let s = S { x: 42 };
+    let p: &dyn T = &s;
+    assert_eq!(std::ptr::metadata(p).size_of(), 4_usize);
+
+    let c: char = 'c';
+    assert_eq!(std::ptr::metadata(&c), ());
 }