From a487eacb681eb7ad59a3f671957acc2b609471cc Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Tue, 8 Aug 2023 18:21:33 +0000
Subject: [PATCH] Breakdown the regression into multiple harnesses

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 .../{extern_c.rs => foreign_functions.rs}     | 33 ++++++++++++++++---
 1 file changed, 28 insertions(+), 5 deletions(-)
 rename tests/kani/Stubbing/{extern_c.rs => foreign_functions.rs} (60%)

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<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);
+}