Fix tests

tautschnig · Jun 11, 2024 · bf7a41e · bf7a41e
1 parent fb35ce0
commit bf7a41e
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -64,8 +64,11 @@ impl<'tcx> GotocCtx<'tcx> {
         span: Option<SpanInternal>,
     ) -> Expr {
         let stable_const = rustc_internal::stable(constant);
-        let stable_span = rustc_internal::stable(span);
-        self.codegen_const_ty(&stable_const, self.codegen_span_stable(stable_span.unwrap()))
+        if let Some(stable_span) = rustc_internal::stable(span) {
+            self.codegen_const_ty(&stable_const, self.codegen_span_stable(stable_span))
+        } else {
+            self.codegen_const_ty(&stable_const, Location::none())
+        }
     }
 
     /// Generate a goto expression that represents a MIR-level constant.

diff --git a/tests/ui/missing-function/extern_c/expected b/tests/ui/missing-function/extern_c/expected
@@ -1,4 +1,4 @@
-Status: UNDETERMINED\
+Status: UNREACHABLE\
 Description: "assertion failed: x == 5"
 Status: FAILURE\
 Description: "Function `missing_function` with missing definition is unreachable"