diff --git a/tests/kani/Stubbing/extern_c.rs b/tests/kani/Stubbing/foreign_functions.rs similarity index 60% rename from tests/kani/Stubbing/extern_c.rs rename to tests/kani/Stubbing/foreign_functions.rs index c99ac328e4e1..7e2abd57912b 100644 --- a/tests/kani/Stubbing/extern_c.rs +++ b/tests/kani/Stubbing/foreign_functions.rs @@ -3,7 +3,7 @@ // // kani-flags: --harness harness --enable-unstable --enable-stubbing // -//! Check support for stubbing out extern C functions. +//! Check support for stubbing out foreign functions. #![feature(rustc_private)] extern crate libc; @@ -39,15 +39,38 @@ fn deeper_call() { dig_deeper(libc::_SC_PAGESIZE) } +fn function_pointer_call(function_pointer: unsafe extern "C" fn(c_int) -> c_longlong) { + assert_eq!(unsafe { function_pointer(libc::_SC_PAGESIZE) } as usize, 10); +} + #[kani::proof] #[kani::stub(libc::strlen, stubs::strlen)] -#[kani::stub(libc::sysconf, stubs::sysconf)] -fn harness() { +fn standard() { let str: Box = Box::new(4); 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(); +} + +#[kani::proof] +#[kani::stub(libc::strlen, stubs::strlen)] +fn function_pointer_standard() { + let str: Box = Box::new(4); + let str_ptr: *const i8 = &*str; let new_ptr = libc::strlen; assert_eq!(unsafe { new_ptr(str_ptr) }, 4); } + +#[kani::proof] +#[kani::stub(libc::sysconf, stubs::sysconf)] +fn function_pointer_with_layers() { + deeper_call(); +} + +#[kani::proof] +#[kani::stub(libc::sysconf, stubs::sysconf)] +fn function_pointer_as_parameter() { + type FunctionPointerType = unsafe extern "C" fn(c_int) -> c_longlong; + let function_pointer: FunctionPointerType = libc::sysconf; + function_pointer_call(function_pointer); + function_pointer_call(libc::sysconf); +}