diff --git a/flake.lock b/flake.lock index a165f224..c882537e 100644 --- a/flake.lock +++ b/flake.lock @@ -9,11 +9,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1759492050, - "narHash": "sha256-C2JH5chm5XWbPdt9xd8PLeDZiXd3Kywr+38BVDjhD4E=", + "lastModified": 1759502955, + "narHash": "sha256-DH9FwoTLY6wPBwnL/DPdSeBZnuNbGKNbA2kT6QJlfPo=", "owner": "aeneasverif", "repo": "charon", - "rev": "fd1c08e51e60be9bd9aecbc2c97f01b985a9a8d4", + "rev": "b51c1fcb513d7c41a5c2a6d73b5cca4d3ad908a8", "type": "github" }, "original": { diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 54fa4f23..c56f900f 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -1766,6 +1766,7 @@ let expression_of_rvalue (env : env) (p : C.rvalue) expected_ty : K.expr = (* The following are `type`s *) | C.CastFnPtr (f, t) | C.CastRawPtr (f, t) | C.CastUnsize (f, t, _) | C.CastTransmute (f, t) -> f = t + | C.CastConcretize _ -> false in if is_ident then expression_of_operand env e