Add BuiltinAssertKinds for Coroutine-related errors

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"

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 }

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) :

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) :

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

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

charon/src/pretty/fmt_with_ctx.rs

@@ -98,6 +98,9 @@ impl<C: AstFormatter> FmtWithCtx<C> 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"),
         }
     }
 }