Skip to content

Commit 4a919cb

Browse files
Update Charon submodule to v0.1.69 (#4660)
Advance the Charon pin from v0.1.68 (63f7749d) to v0.1.69 (485bd36e), the next step of the incremental effort to catch the pinned Charon up with upstream (the endgame is dropping scripts/charon-patch.diff entirely). Charon v0.1.69 makes `Vector::elem_count` the way to obtain the number of non-empty slots (`len` is removed); adapt the tuple-field-projection translation in the LLBC backend accordingly. Refresh scripts/charon-patch.diff so its hunks apply against the v0.1.69 sources (context-line drift only; the patch content is unchanged). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
1 parent 68d40b8 commit 4a919cb

4 files changed

Lines changed: 8 additions & 8 deletions

File tree

Cargo.lock

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -288,7 +288,7 @@ checksum = "f079e83a288787bcd14a6aea84cee5c87a67c5a3e660c30f557a3d24761b3527"
288288

289289
[[package]]
290290
name = "charon"
291-
version = "0.1.68"
291+
version = "0.1.69"
292292
dependencies = [
293293
"annotate-snippets",
294294
"anstream 0.6.21",

charon

Submodule charon updated 155 files

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1873,7 +1873,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
18731873
}
18741874
}
18751875
CharonTyKind::Adt(CharonTypeId::Tuple, genargs) => {
1876-
let c_fprj = CharonFieldProjKind::Tuple(genargs.types.len());
1876+
let c_fprj = CharonFieldProjKind::Tuple(genargs.types.elem_count());
18771877
current_ty = self.translate_ty(*ty);
18781878
c_provec.push((
18791879
CharonProjectionElem::Field(c_fprj, c_fieldid),

scripts/charon-patch.diff

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,21 +1,21 @@
11
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
2-
index d76c223c..0b354b1c 100644
2+
index cbba6280f..8b5b4ece8 100644
33
--- a/charon/Cargo.toml
44
+++ b/charon/Cargo.toml
55
@@ -2,7 +2,7 @@
66
name = "charon"
7-
version = "0.1.68"
7+
version = "0.1.69"
88
authors = ["Son Ho <hosonmarc@gmail.com>"]
99
-edition = "2021"
1010
+edition = "2024"
1111
license = "Apache-2.0"
1212

1313
[lib]
1414
diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs
15-
index 141cabe3..37948679 100644
15+
index 24dd10839..3ef70b0bc 100644
1616
--- a/charon/src/ids/vector.rs
1717
+++ b/charon/src/ids/vector.rs
18-
@@ -254,7 +254,7 @@ where
18+
@@ -260,7 +260,7 @@ where
1919
self.iter_indexed().map(|(id, _)| id)
2020
}
2121

@@ -25,7 +25,7 @@ index 141cabe3..37948679 100644
2525
}
2626

2727
diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs
28-
index 225da182..54370990 100644
28+
index 2b8a5d162..4716da208 100644
2929
--- a/charon/src/transform/expand_associated_types.rs
3030
+++ b/charon/src/transform/expand_associated_types.rs
3131
@@ -761,7 +761,7 @@ impl<'a> ComputeItemModifications<'a> {

0 commit comments

Comments
 (0)