From 74cd0502425e6987eb79f844f88c71a858623bd7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 4 Jul 2025 13:56:51 +0200 Subject: [PATCH] Update charon --- flake.lock | 6 +++--- lib/AstOfLlbc.ml | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/flake.lock b/flake.lock index 44df3f24..ef1ff1d2 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1751475806, - "narHash": "sha256-JJ+h/atDD8GCu36UhzcmKo89v1ySB6m6mqHjuDpJtcY=", + "lastModified": 1751634443, + "narHash": "sha256-g4XH70eVCruLMtSyXnRqGQIkv6h9mv8BpXYfX8OuERQ=", "owner": "aeneasverif", "repo": "charon", - "rev": "ccaf6c6f718487192ecad3ce447c161835a61262", + "rev": "91b5a914e7f6fb78fd26ff6bafed05676e5f8d33", "type": "github" }, "original": { diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index a3db5cc4..2a23373f 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1943,7 +1943,7 @@ and expression_of_raw_statement (env : env) (ret_var : C.local_id) (s : C.raw_st | SetDiscriminant (_, _) -> failwith "C.SetDiscriminant" | StorageLive _ -> Krml.Helpers.eunit | StorageDead _ -> Krml.Helpers.eunit - | Deinit p | Drop p -> + | Deinit p | Drop (p, _) -> let _ = expression_of_place env p in begin match p.ty with