Skip to content

Update charon submodule by 15 commits #4464

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
zhassan-aws merged 1 commit into from
Nov 11, 2025
Merged

Update charon submodule by 15 commits #4464

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion Cargo.lock
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -248,7 +248,7 @@ checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"

[[package]]
name = "charon"
version = "0.1.65"
version = "0.1.67"
dependencies = [
"annotate-snippets",
"anstream",
Expand Down Expand Up @@ -940,6 +940,7 @@ dependencies = [
"charon",
"clap",
"cprover_bindings",
"indexmap",
"itertools 0.14.0",
"kani_metadata",
"lazy_static",
Expand Down
2 changes: 1 addition & 1 deletion charon
Open in desktop
Submodule charon updated 51 files
+1 −1 charon-ml/src/CharonVersion.ml
+6 −0 charon-ml/src/generated/Generated_GAst.ml
+6 −0 charon-ml/src/generated/Generated_GAstOfJson.ml
+1 −1 charon/Cargo.lock
+1 −4 charon/Cargo.toml
+3 −3 charon/src/ast/gast.rs
+22 −5 charon/src/ast/llbc_ast_utils.rs
+2 −3 charon/src/ast/meta.rs
+24 −9 charon/src/ast/ullbc_ast_utils.rs
+19 −0 charon/src/ast/visitor.rs
+43 −7 charon/src/bin/charon-driver/translate/translate_ctx.rs
+8 −1 charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
+35 −31 charon/src/bin/charon-driver/translate/translate_traits.rs
+12 −10 charon/src/bin/charon/main.rs
+1 −16 charon/src/bin/generate-ml/main.rs
+18 −0 charon/src/lib.rs
+9 −0 charon/src/options.rs
+3 −0 charon/src/transform/mod.rs
+24 −0 charon/src/transform/remove_unused_methods.rs
+0 −12 charon/tests/ui/associated-types.out
+0 −9 charon/tests/ui/call-to-known-trait-method.out
+0 −3 charon/tests/ui/closures.out
+0 −3 charon/tests/ui/external.out
+14 −14 charon/tests/ui/generic-associated-types.out
+0 −3 charon/tests/ui/impl-trait.out
+0 −3 charon/tests/ui/issue-118-generic-copy.out
+0 −3 charon/tests/ui/issue-165-vec-macro.out
+189 −1,102 charon/tests/ui/issue-297-cfg.out
+52 −940 charon/tests/ui/issue-395-failed-to-normalize.out
+0 −3 charon/tests/ui/issue-4-slice-try-into-array.out
+0 −3 charon/tests/ui/issue-4-traits.out
+213 −1,197 charon/tests/ui/issue-45-misc.out
+0 −12 charon/tests/ui/issue-70-override-provided-method.3.out
+0 −33 charon/tests/ui/issue-70-override-provided-method.out
+0 −3 charon/tests/ui/issue-91-enum-to-discriminant-cast.out
+32 −32 charon/tests/ui/iterator.out
+3 −2 charon/tests/ui/iterator.rs
+207 −1,237 charon/tests/ui/loops.out
+0 −3 charon/tests/ui/method-impl-generalization.out
+153 −0 charon/tests/ui/opaque-trait.out
+48 −0 charon/tests/ui/opaque-trait.rs
+0 −3 charon/tests/ui/opaque_attribute.out
+3 −78 charon/tests/ui/polonius_map.out
+0 −3 charon/tests/ui/predicates-on-late-bound-vars.out
+49 −928 charon/tests/ui/quantified-clause.out
+24 −0 charon/tests/ui/simple/opaque-trait-with-clause-in-method.out
+11 −0 charon/tests/ui/simple/opaque-trait-with-clause-in-method.rs
+0 −12 charon/tests/ui/type_alias.out
+213 −1,216 charon/tests/ui/ullbc-control-flow.out
+0 −6 charon/tests/ui/unsize.out
+47 −1,049 charon/tests/ui/unsupported/issue-79-bound-regions.out
1 change: 1 addition & 0 deletions kani-compiler/Cargo.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ publish = false
cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
charon = { path = "../charon/charon", optional = true, default-features = false }
clap = { version = "4.4.11", features = ["derive", "cargo"] }
indexmap = { version = "2.7.1", features = ["serde"] }
itertools = "0.14"
kani_metadata = { path = "../kani_metadata" }
lazy_static = "1.5.0"
Expand Down
1 change: 0 additions & 1 deletion kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,6 @@ use rustc_session::Session;
use rustc_session::config::{CrateType, OutputFilenames, OutputType};
use rustc_session::output::out_filename;
use std::any::Any;
use std::cell::RefCell;
use std::fs::File;
use std::path::Path;
use std::sync::{Arc, Mutex};
Expand Down
9 changes: 3 additions & 6 deletions kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ use charon_lib::ullbc_ast::{
};
use charon_lib::{error_assert, raise_error, register_error};
use core::panic;
use indexmap::IndexMap;
use rustc_data_structures::fx::FxHashMap;
use rustc_middle::ty::{TyCtxt, TypingEnv};
use rustc_public::mir::mono::{Instance, InstanceDef};
Expand Down Expand Up @@ -118,21 +119,17 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
self.errors.span_err(self.translated, span, msg)
}

fn continue_on_failure(&self) -> bool {
self.errors.continue_on_failure()
}

fn translate_traitdecl(&mut self, trait_def: TraitDef) -> CharonTraitDeclId {
let trait_def_id = trait_def.def_id();
let trait_decl_id = self.register_trait_decl_id(trait_def_id);
match self.translated.trait_decls.get(trait_decl_id) {
None => {
let trait_decl = TraitDef::declaration(&trait_def);
let consts = Vec::new();
let const_defaults = HashMap::new();
let const_defaults = IndexMap::new();
let types = Vec::new();
let type_clauses = Vec::new();
let type_defaults = HashMap::new();
let type_defaults = IndexMap::new();
let required_methods = Vec::new();
let provided_methods = Vec::new();
let parent_clauses = CharonVector::new();
Expand Down
2 changes: 1 addition & 1 deletion scripts/charon-patch.diff
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ index 20f8a9df..a1bf1ee6 100644
+++ b/charon/Cargo.toml
@@ -2,7 +2,7 @@
name = "charon"
version = "0.1.65"
version = "0.1.67"
authors = ["Son Ho <hosonmarc@gmail.com>"]
-edition = "2021"
+edition = "2024"
Expand Down
Loading