From 712f1f52ad50f6b985c76af83a3875f35ae195f8 Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 15 May 2026 09:31:27 +0100 Subject: [PATCH] Bump Charon --- charon-pin | 2 +- flake.lock | 6 +++--- src/PrePasses.ml | 8 ++------ src/interp/InterpStatements.ml | 3 --- src/interp/InterpUtils.ml | 3 +-- src/llbc/FunsAnalysis.ml | 3 +-- tests/coq/demo/Demo.v | 4 ++-- tests/fstar/demo/Demo.fst | 4 ++-- tests/lean/Derive.lean | 2 +- 9 files changed, 13 insertions(+), 22 deletions(-) diff --git a/charon-pin b/charon-pin index 965b39bc3..25e8dae7b 100644 --- a/charon-pin +++ b/charon-pin @@ -1,2 +1,2 @@ # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas. -b1096182b418d99fa7440421dcf1099fda5785ae +103daa06617306f28c2515e87efdcfc1a94dc7a2 diff --git a/flake.lock b/flake.lock index 46db08e09..fdd3d7a47 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1779962030, - "narHash": "sha256-TqjxmAPVNcbZ/7spKFFSrZwUV/AWvFUZ5cu7Oh76KVw=", + "lastModified": 1779976260, + "narHash": "sha256-YI0l3Av/MrvIunGQ0p1mImPckvM+hXofuAOrnQNMSIA=", "owner": "aeneasverif", "repo": "charon", - "rev": "b1096182b418d99fa7440421dcf1099fda5785ae", + "rev": "103daa06617306f28c2515e87efdcfc1a94dc7a2", "type": "github" }, "original": { diff --git a/src/PrePasses.ml b/src/PrePasses.ml index 81db84fd6..8b04bc0fe 100644 --- a/src/PrePasses.ml +++ b/src/PrePasses.ml @@ -747,12 +747,8 @@ let remove_useless_joins (crate : crate) (f : fun_decl) : fun_decl = match rv with | Use _ | RvRef _ | RawPtr _ | NullaryOp _ | Aggregate _ -> (can_inline, st :: ls) - | BinaryOp _ - | UnaryOp _ - | Discriminant _ - | Len _ - | Repeat _ - | ShallowInitBox _ -> (false, st :: ls)) + | BinaryOp _ | UnaryOp _ | Discriminant _ | Len _ | Repeat _ -> + (false, st :: ls)) | SetDiscriminant _ | CopyNonOverlapping _ | Assert _ | Call _ | Error _ -> (false, st :: ls)) in diff --git a/src/interp/InterpStatements.ml b/src/interp/InterpStatements.ml index 0b437ee80..b79b3e425 100644 --- a/src/interp/InterpStatements.ml +++ b/src/interp/InterpStatements.ml @@ -847,9 +847,6 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun = | Repeat _ -> [%craise] st.span "Repeat should have been removed in a micropass" - | ShallowInitBox _ -> - [%craise] st.span - "ShallowInitBox should have been removed in a micropass" | Use _ | RvRef ( _, diff --git a/src/interp/InterpUtils.ml b/src/interp/InterpUtils.ml index cd9adbb1a..4233a28e8 100644 --- a/src/interp/InterpUtils.ml +++ b/src/interp/InterpUtils.ml @@ -447,8 +447,7 @@ let rvalue_get_place (rv : rvalue) : place option = | BinaryOp _ | Discriminant _ | Aggregate _ - | Repeat _ - | ShallowInitBox _ -> None + | Repeat _ -> None (** See {!ValuesUtils.symbolic_value_has_borrows} *) let symbolic_value_has_borrows span (ctx : eval_ctx) (sv : symbolic_value) : diff --git a/src/llbc/FunsAnalysis.ml b/src/llbc/FunsAnalysis.ml index 1ff263eca..657e15862 100644 --- a/src/llbc/FunsAnalysis.ml +++ b/src/llbc/FunsAnalysis.ml @@ -120,8 +120,7 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) : | Len _ | NullaryOp _ | RawPtr _ - | Repeat _ - | ShallowInitBox _ -> () + | Repeat _ -> () | RvRef ({ kind = PlaceGlobal gref; _ }, _, _) -> ( (* A reference to a global: propagate can_fail. diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v index eb6ed1639..94de38fc5 100644 --- a/tests/coq/demo/Demo.v +++ b/tests/coq/demo/Demo.v @@ -9,13 +9,13 @@ Local Open Scope Primitives_scope. Module Demo. (** [core::num::{u32}::wrapping_add]: - Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2397:8-2397:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2456:8-2456:58 Name pattern: [core::num::{u32}::wrapping_add] Visibility: public *) Axiom core_num_U32_wrapping_add : u32 -> u32 -> result u32. (** [core::num::{u32}::wrapping_sub]: - Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2434:8-2434:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2493:8-2493:58 Name pattern: [core::num::{u32}::wrapping_sub] Visibility: public *) Axiom core_num_U32_wrapping_sub : u32 -> u32 -> result u32. diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst index a7685ee39..31630eeca 100644 --- a/tests/fstar/demo/Demo.fst +++ b/tests/fstar/demo/Demo.fst @@ -6,13 +6,13 @@ open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" (** [core::num::{u32}::wrapping_add]: - Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2397:8-2397:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2456:8-2456:58 Name pattern: [core::num::{u32}::wrapping_add] Visibility: public *) assume val core_num_U32_wrapping_add : u32 -> u32 -> result u32 (** [core::num::{u32}::wrapping_sub]: - Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2434:8-2434:58 + Source: '/rustc/library/core/src/num/uint_macros.rs', lines 2493:8-2493:58 Name pattern: [core::num::{u32}::wrapping_sub] Visibility: public *) assume val core_num_U32_wrapping_sub : u32 -> u32 -> result u32 diff --git a/tests/lean/Derive.lean b/tests/lean/Derive.lean index 324205454..22e7bfce5 100644 --- a/tests/lean/Derive.lean +++ b/tests/lean/Derive.lean @@ -25,7 +25,7 @@ namespace derive axiom Bool.Insts.CoreCmpPartialEqBool.ne : Bool → Bool → Result Bool /-- [alloc::boxed::{core::cmp::PartialEq> for alloc::boxed::Box}::ne]: - Source: '/rustc/library/alloc/src/boxed.rs', lines 2056:4-2056:38 + Source: '/rustc/library/alloc/src/boxed.rs', lines 2100:4-2100:38 Name pattern: [alloc::boxed::{core::cmp::PartialEq, Box<@T>>}::ne] Visibility: public -/ @[rust_fun "alloc::boxed::{core::cmp::PartialEq, Box<@T>>}::ne"]