From 62b4b545fff72ce98a1786e8e184fe7a0fa65be3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 18 Nov 2024 11:44:46 +0100 Subject: [PATCH] Update charon --- flake.lock | 12 ++++++------ lib/AstOfLlbc.ml | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/flake.lock b/flake.lock index 921a1b9..53766f9 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1731507985, - "narHash": "sha256-G5v5nFT6ixI5FpmixIDrXQma2A6GJQ90XqGPgl4jOHc=", + "lastModified": 1731923767, + "narHash": "sha256-l7+5K3Fftx0M7CypqDrBEz0puoEqD6YB1XUm6ONwY20=", "owner": "aeneasverif", "repo": "charon", - "rev": "d812e51376d89753900bf3cfdd87b15c53157970", + "rev": "8eb499486be56a96317ce967f208cce1a1d4477f", "type": "github" }, "original": { @@ -240,11 +240,11 @@ ] }, "locked": { - "lastModified": 1731464916, - "narHash": "sha256-WZ5rpjr/wCt7yBOUsvDE2i22hYz9g8W921jlwVktRQ4=", + "lastModified": 1731897198, + "narHash": "sha256-Ou7vLETSKwmE/HRQz4cImXXJBr/k9gp4J4z/PF8LzTE=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "2c19bad6e881b5a154cafb7f9106879b5b356d1f", + "rev": "0be641045af6d8666c11c2c40e45ffc9667839b5", "type": "github" }, "original": { diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 9ffc249..f5ef049 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1646,7 +1646,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = match decl with | None -> None | Some decl -> ( - let { C.def_id; signature; body; is_global_decl_body; item_meta; kind; _ } = decl in + let { C.def_id; signature; body; item_meta; kind; _ } = decl in let env = { env with generic_params = signature.generics } in L.log "AstOfLlbc" "Visiting %sfunction: %s\n%s" (if body = None then @@ -1668,7 +1668,7 @@ let decl_of_id (env : env) (id : C.any_decl_id) : K.decl option = let { K.n_cgs; n }, t = typ_of_signature env signature in Some (K.DExternal (None, [], n_cgs, n, name, t, [])) | Some { locals; body; _ }, _ -> - if is_global_decl_body then + if signature.is_global_initializer then None else let env = push_cg_binders env signature.C.generics.const_generics in