diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index d7d76bb54f81..148318f1c33e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -299,6 +299,20 @@ impl<'tcx> GotocCtx<'tcx> { &self.symbol_table, ) } + // TODO: Improve this check after we upgrade nightly to 2023-12-18. + TyKind::RigidTy(RigidTy::Adt(def, _)) if def.name().ends_with("::CStr") => { + // TODO: Handle CString + // + let loc = self.codegen_span_option_stable(span); + let typ = self.codegen_ty_stable(ty); + let operation_name = "C string literal"; + self.codegen_unimplemented_expr( + &operation_name, + typ, + loc, + "https://github.com/model-checking/kani/issues/2549", + ) + } _ => unreachable!("{inner_ty:?}"), } } else if !alloc.provenance.ptrs.is_empty() { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 36485170136c..5c17a2e4df62 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-12-14" +channel = "nightly-2023-12-15" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]