Breakdown the regression into multiple harnesses

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
model-checking · Aug 8, 2023 · 2d84403 · 2d84403
1 parent 420905d
commit 2d84403
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 7 deletions.
diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs
@@ -69,7 +69,9 @@ impl<'tcx> MutVisitor<'tcx> for ForeignFunctionTransformer<'tcx> {
         if let ty::FnDef(reachable_function, generics) = *func_ty.kind() {
             if self.tcx.is_foreign_item(reachable_function) {
                 if let Some(stub) = self.stub_map.get(&reachable_function) {
-                    let Operand::Constant(function_definition) = operand else { return; };
+                    let Operand::Constant(function_definition) = operand else {
+                        return;
+                    };
                     function_definition.literal = ConstantKind::from_value(
                         ConstValue::ZeroSized,
                         self.tcx.type_of(stub).subst(self.tcx, generics),

diff --git a/tests/kani/Stubbing/extern_c.rs → tests/kani/Stubbing/foreign_functions.rs b/tests/kani/Stubbing/extern_c.rs → tests/kani/Stubbing/foreign_functions.rs
@@ -1,9 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness harness --enable-unstable --enable-stubbing
+// kani-flags: --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);
+}