Breakdown the regression into multiple harnesses

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

tests/kani/Stubbing/extern_c.rs → 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<i8> = 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<i8> = 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);
+}