Add function-pointer test case without generic type

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
model-checking · Aug 8, 2023 · 3cde065 · 3cde065
1 parent 78f77ff
commit 3cde065
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 11 deletions.
diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs
@@ -36,17 +36,15 @@ pub fn transform<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId, old_body: &'tcx Body<'t
     old_body.clone()
 }
 
-/// Tranverse `body` searching for calls to foreing functions and, whevever there is
+/// Traverse `body` searching for calls to foreing functions and, whevever there is
 /// a stub available, replace the call to the foreign function with a call
 /// to its correspondent stub. This happens as a separate step because there is no
 /// body available to foreign functions at this stage.
 pub fn transform_foreign_functions<'tcx>(tcx: TyCtxt<'tcx>, body: &mut Body<'tcx>) {
-    let mut visitor = if let Some(stub_map) = get_stub_mapping(tcx) {
-        ForeignFunctionTransformer { tcx, body: body.clone(), stub_map }
-    } else {
-        ForeignFunctionTransformer { tcx, body: body.clone(), stub_map: HashMap::default() }
-    };
-    visitor.visit_body(body);
+    if let Some(stub_map) = get_stub_mapping(tcx) {
+        let mut visitor = ForeignFunctionTransformer { tcx, body: body.clone(), stub_map };
+        visitor.visit_body(body);
+    }
 }
 
 struct ForeignFunctionTransformer<'tcx> {
@@ -68,8 +66,8 @@ 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(fn_def) = operand else { unreachable!() };
-                    fn_def.literal = ConstantKind::from_value(
+                    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 b/tests/kani/Stubbing/extern_c.rs
@@ -27,7 +27,7 @@ mod stubs {
     }
 }
 
-fn dig_depper(input : c_int) {
+fn dig_deeper(input: c_int) {
     unsafe {
         type FunctionPointerType = unsafe extern "C" fn(c_int) -> c_longlong;
         let ptr: FunctionPointerType = libc::sysconf;
@@ -36,7 +36,7 @@ fn dig_depper(input : c_int) {
 }
 
 fn deeper_call() {
-    dig_depper(libc::_SC_PAGESIZE)
+    dig_deeper(libc::_SC_PAGESIZE)
 }
 
 #[kani::proof]
@@ -48,4 +48,6 @@ fn harness() {
     assert_eq!(unsafe { libc::strlen(str_ptr) }, 4);
     assert_eq!(unsafe { libc::sysconf(libc::_SC_PAGESIZE) } as usize, 10);
     deeper_call();
+    let new_ptr = libc::strlen;
+    assert_eq!(unsafe { new_ptr(str_ptr) }, 4);
 }