Skip to content

Commit

Permalink
Add test case with function pointer
Browse files Browse the repository at this point in the history
Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
  • Loading branch information
feliperodri committed Aug 4, 2023
1 parent d797734 commit 67bc1d3
Showing 1 changed file with 13 additions and 0 deletions.
13 changes: 13 additions & 0 deletions tests/kani/Stubbing/extern_c.rs
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,18 @@ mod stubs {
}
}

fn dig_depper(input : c_int) {
unsafe {
type FunctionPointerType = unsafe extern "C" fn(c_int) -> c_longlong;
let ptr: FunctionPointerType = libc::sysconf;
assert_eq!(ptr(input) as usize, 10);
}
}

fn deeper_call() {
dig_depper(libc::_SC_PAGESIZE)
}

#[kani::proof]
#[kani::stub(libc::strlen, stubs::strlen)]
#[kani::stub(libc::sysconf, stubs::sysconf)]
Expand All @@ -35,4 +47,5 @@ fn harness() {
let str_ptr: *const i8 = &*str;
assert_eq!(unsafe { libc::strlen(str_ptr) }, 4);
assert_eq!(unsafe { libc::sysconf(libc::_SC_PAGESIZE) } as usize, 10);
deeper_call();
}

0 comments on commit 67bc1d3

Please sign in to comment.