Fix tests

tautschnig · Jun 11, 2024 · 2171d7e · 2171d7e
1 parent 23f68ea
commit 2171d7e
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git 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
@@ -1,4 +1,4 @@
-Status: UNREACHABLE\
+Status: UNDETERMINED\
 Description: "assertion failed: x == 5"
 Status: FAILURE\
 Description: "Function `missing_function` with missing definition is unreachable"