Skip to content

Commit

Permalink
Expand test
Browse files Browse the repository at this point in the history
  • Loading branch information
tautschnig committed Jun 10, 2024
1 parent 36a9dd9 commit 60572fc
Showing 1 changed file with 15 additions and 0 deletions.
15 changes: 15 additions & 0 deletions tests/kani/FatPointers/metadata.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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), ());
}

0 comments on commit 60572fc

Please sign in to comment.