From 2171d7e5c74ee64f4b79d1bd7528a245e7d6e266 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 11 Jun 2024 11:29:02 +0000
Subject: [PATCH] Fix tests

---
 tests/cargo-kani/simple-extern/src/lib.rs   | 3 +++
 tests/ui/missing-function/extern_c/expected | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/tests/cargo-kani/simple-extern/src/lib.rs b/tests/cargo-kani/simple-extern/src/lib.rs
index d2016d8bd7b2..33ca290a2d30 100644
--- a/tests/cargo-kani/simple-extern/src/lib.rs
+++ b/tests/cargo-kani/simple-extern/src/lib.rs
@@ -2,6 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 pub mod externs;
 pub use externs::external_c_assertion;
+// TODO: our reachability analysis does not see through C functions
+pub use externs::rust_add1;
 
 #[cfg(test)]
 mod tests {
@@ -24,6 +26,7 @@ mod kani_tests {
         if a < 100 {
             unsafe {
                 external_c_assertion(a);
+                rust_add1(a);
             }
         }
     }
diff --git a/tests/ui/missing-function/extern_c/expected b/tests/ui/missing-function/extern_c/expected
index 412522828a55..eab619abc0d9 100644
--- a/tests/ui/missing-function/extern_c/expected
+++ b/tests/ui/missing-function/extern_c/expected
@@ -1,4 +1,4 @@
-Status: UNREACHABLE\
+Status: UNDETERMINED\
 Description: "assertion failed: x == 5"
 Status: FAILURE\
 Description: "Function `missing_function` with missing definition is unreachable"