Expand test

tautschnig · Jun 10, 2024 · 60572fc · 60572fc
1 parent 36a9dd9
commit 60572fc
Showing 1 changed file with 15 additions and 0 deletions.
diff --git 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), ());
 }