diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index bc2750e8d56b..911a09eac496 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -108,6 +108,13 @@ jobs: with: os: ubuntu-24.04 + # Patch Charon so that it compiles. This is temporary until we're able to + # upgrade the pinned commit which requires fixing + # https://github.com/AeneasVerif/charon/issues/806 and updating the + # mir-to-ullbc code + - name: Patch Charon + run: cd charon && git apply ../scripts/charon-patch.diff + - name: Build Kani with Charon run: cargo build-dev -- --features cprover --features llbc diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index c9a980b25f22..60f2e0f6a101 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -69,6 +69,7 @@ use rustc_public::ty::{ Ty, TyConst, TyConstKind, TyKind, UintTy, }; use rustc_public::{CrateDef, CrateDefType, DefId}; +use rustc_public_bridge::IndexedVal; use std::collections::HashMap; use std::iter::zip; use std::path::PathBuf; @@ -1009,7 +1010,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { name.push(CharonPathElem::Ident(crate_name, CharonDisambiguator::new(0))); } - if let Some(impl_defid_internal) = self.tcx.impl_of_method(def_id) { + if let Some(impl_defid_internal) = self.tcx.impl_of_assoc(def_id) { let traitref = self .tcx .impl_trait_ref(impl_defid_internal) diff --git a/scripts/charon-patch.diff b/scripts/charon-patch.diff new file mode 100644 index 000000000000..543be483244d --- /dev/null +++ b/scripts/charon-patch.diff @@ -0,0 +1,26 @@ +diff --git a/charon/Cargo.toml b/charon/Cargo.toml +index 20f8a9df..a1bf1ee6 100644 +--- a/charon/Cargo.toml ++++ b/charon/Cargo.toml +@@ -2,7 +2,7 @@ + name = "charon" + version = "0.1.62" + authors = ["Son Ho "] +-edition = "2021" ++edition = "2024" + license = "Apache-2.0" + + [lib] +diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs +index 59f7eaab..21508e19 100644 +--- a/charon/src/ids/vector.rs ++++ b/charon/src/ids/vector.rs +@@ -217,7 +217,7 @@ where + self.iter_indexed().map(|(id, _)| id) + } + +- pub fn all_indices(&self) -> impl Iterator { ++ pub fn all_indices(&self) -> impl Iterator + use { + self.vector.indices() + } +