diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 3c46404f71bc..687761e134a7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -128,7 +128,8 @@ impl<'tcx> GotocCtx<'tcx> { ConstValue::Slice { data, start, end } => { self.codegen_slice_value(v, lit_ty, span, data.inner(), start, end) } - ConstValue::ByRef { alloc, offset } => { + ConstValue::Indirect { alloc_id, offset } => { + let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory(); debug!("ConstValue by ref {:?} {:?}", alloc, offset); let mem_var = self.codegen_const_allocation(alloc.inner(), None); mem_var diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 666344e012f0..38a90686abc1 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -34,7 +34,6 @@ use rustc_hir::definitions::DefPathHash; use rustc_interface::Config; use rustc_middle::ty::TyCtxt; use rustc_session::config::{ErrorOutputType, OutputType}; -use rustc_session::EarlyErrorHandler; use rustc_span::ErrorGuaranteed; use std::collections::{BTreeMap, HashMap}; use std::fs::File; @@ -396,7 +395,6 @@ impl Callbacks for KaniCompiler { /// During the initialization state, we collect the crate harnesses and prepare for codegen. fn after_analysis<'tcx>( &mut self, - _handler: &EarlyErrorHandler, _compiler: &rustc_interface::interface::Compiler, rustc_queries: &'tcx rustc_interface::Queries<'tcx>, ) -> Compilation { diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 466bad80e569..42afeefb81df 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -320,8 +320,13 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { ConstValue::Scalar(Scalar::Ptr(ptr, _size)) => { self.collected.extend(collect_alloc_items(self.tcx, ptr.provenance).iter()); } - ConstValue::Slice { data: alloc, start: _, end: _ } - | ConstValue::ByRef { alloc, .. } => { + ConstValue::Slice { data: alloc, start: _, end: _ } => { + for id in alloc.inner().provenance().provenances() { + self.collected.extend(collect_alloc_items(self.tcx, id).iter()) + } + } + ConstValue::Indirect { alloc_id, .. } => { + let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory(); for id in alloc.inner().provenance().provenances() { self.collected.extend(collect_alloc_items(self.tcx, id).iter()) } diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 620bb2915511..c70658e0de73 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-09-11" +channel = "nightly-2023-09-15" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]