From a8b7192156d8982725760f094efaac38ab1874ce Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 19 Apr 2026 16:00:06 +0100 Subject: [PATCH 1/4] Add BuiltinAssertKinds for Coroutine-related errors Signed-off-by: Sacha Ayoun --- charon/src/ast/gast.rs | 3 +++ charon/src/pretty/fmt_with_ctx.rs | 3 +++ 2 files changed, 6 insertions(+) diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 1851b1cd9..9992bd603 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -494,6 +494,9 @@ pub enum BuiltinAssertKind { MisalignedPointerDereference { required: Operand, found: Operand }, NullPointerDereference, InvalidEnumConstruction(Operand), + ResumedAfterReturn, + ResumedAfterPanic, + ResumedAfterDrop, } /// (U)LLBC is a language with side-effects: a statement may abort in a way that isn't tracked by diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 37499e08c..c3ae7607d 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -98,6 +98,9 @@ impl FmtWithCtx for BuiltinAssertKind { BuiltinAssertKind::InvalidEnumConstruction(..) => { write!(f, "invalid_enum_construction") } + BuiltinAssertKind::ResumedAfterReturn => write!(f, "resumed_after_return"), + BuiltinAssertKind::ResumedAfterDrop => write!(f, "resumed_after_drop"), + BuiltinAssertKind::ResumedAfterPanic => write!(f, "resumed_after_panic"), } } } From 08fb22ebb5990ce6f94bd7fe57d08988228a9e7f Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sun, 19 Apr 2026 17:02:46 +0100 Subject: [PATCH 2/4] generate-ml Signed-off-by: Sacha Ayoun --- charon-ml/src/generated/Generated_GAst.ml | 3 +++ charon-ml/src/generated/Generated_OfJson.ml | 3 +++ 2 files changed, 6 insertions(+) diff --git a/charon-ml/src/generated/Generated_GAst.ml b/charon-ml/src/generated/Generated_GAst.ml index 823c8dccb..82c6a493a 100644 --- a/charon-ml/src/generated/Generated_GAst.ml +++ b/charon-ml/src/generated/Generated_GAst.ml @@ -76,6 +76,9 @@ and builtin_assert_kind = - [found] *) | NullPointerDereference | InvalidEnumConstruction of operand + | ResumedAfterReturn + | ResumedAfterPanic + | ResumedAfterDrop and call = { func : fn_operand; args : operand list; dest : place } and copy_non_overlapping = { src : operand; dst : operand; count : operand } diff --git a/charon-ml/src/generated/Generated_OfJson.ml b/charon-ml/src/generated/Generated_OfJson.ml index 1a5e3fff3..4564b3d92 100644 --- a/charon-ml/src/generated/Generated_OfJson.ml +++ b/charon-ml/src/generated/Generated_OfJson.ml @@ -265,6 +265,9 @@ and builtin_assert_kind_of_json (ctx : of_json_ctx) (js : json) : operand_of_json ctx invalid_enum_construction in Ok (InvalidEnumConstruction invalid_enum_construction) + | `String "ResumedAfterReturn" -> Ok ResumedAfterReturn + | `String "ResumedAfterPanic" -> Ok ResumedAfterPanic + | `String "ResumedAfterDrop" -> Ok ResumedAfterDrop | _ -> Error "") and builtin_fun_id_of_json (ctx : of_json_ctx) (js : json) : From dd95c1c1e146dc7fc104eb3b55c360153fb3376b Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 16 May 2026 00:02:22 +0100 Subject: [PATCH 3/4] regenerate ml after rebase Signed-off-by: Sacha Ayoun --- charon-ml/src/generated/Generated_OfPostcard.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/charon-ml/src/generated/Generated_OfPostcard.ml b/charon-ml/src/generated/Generated_OfPostcard.ml index de9f4ec1c..d46e3d8ac 100644 --- a/charon-ml/src/generated/Generated_OfPostcard.ml +++ b/charon-ml/src/generated/Generated_OfPostcard.ml @@ -243,6 +243,9 @@ and builtin_assert_kind_of_postcard (ctx : of_postcard_ctx) | 7 -> let* x_0 = operand_of_postcard ctx st in Ok (InvalidEnumConstruction x_0) + | 8 -> Ok ResumedAfterReturn + | 9 -> Ok ResumedAfterPanic + | 10 -> Ok ResumedAfterDrop | _ -> Error ("unknown enum variant tag: " ^ string_of_int __tag)) and builtin_fun_id_of_postcard (ctx : of_postcard_ctx) (st : postcard_state) : From ea401dc7a006868068953aefe61480c1c883a231 Mon Sep 17 00:00:00 2001 From: Sacha Ayoun Date: Sat, 16 May 2026 00:07:52 +0100 Subject: [PATCH 4/4] update version Signed-off-by: Sacha Ayoun --- charon-ml/src/CharonVersion.ml | 2 +- charon/Cargo.lock | 2 +- charon/Cargo.toml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index b14cdfef3..b5f8e3708 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.196" +let supported_charon_version = "0.1.197" diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 5a9f418ab..6c6bd0976 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -252,7 +252,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.196" +version = "0.1.197" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 9a333eaa7..f185d2639 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -24,7 +24,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] } [package] name = "charon" -version = "0.1.196" +version = "0.1.197" authors.workspace = true edition.workspace = true license.workspace = true