diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 6ea252b9bb95..ed177b4d1708 100644 --- 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, ) -> 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 index eab619abc0d9..412522828a55 100644 --- 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"