diff --git a/flake.lock b/flake.lock index 1589425..0a2d4c2 100644 --- a/flake.lock +++ b/flake.lock @@ -11,11 +11,11 @@ "rust-overlay": "rust-overlay" }, "locked": { - "lastModified": 1724239793, - "narHash": "sha256-aiR5BVfWpkzZWR1WZbMhqcuDAvznV5fq2nBDCqQEczc=", + "lastModified": 1724768110, + "narHash": "sha256-PPjuaIQa9srw64rDeaatDf3CHPNgLbqwfE0DSdEU37Q=", "owner": "aeneasverif", "repo": "charon", - "rev": "9e782beeb099f447661ce91da9ba1181a94642fe", + "rev": "13502d2f3bd477ee86acafe5974016dc7707db83", "type": "github" }, "original": { @@ -246,11 +246,11 @@ ] }, "locked": { - "lastModified": 1724206841, - "narHash": "sha256-L8dKaX4T3k+TR2fEHCfGbH4UXdspovz/pj87iai9qmc=", + "lastModified": 1724725307, + "narHash": "sha256-gnu8JrUFQoy7b927EPuwmWpvk8MSroFl07pplmVueYA=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "45e98fbd62c32e5927e952d2833fa1ba4fb35a61", + "rev": "f56076b216c266cd855b0811ceb86802e834cdb9", "type": "github" }, "original": { diff --git a/lib/AstOfLlbc.ml b/lib/AstOfLlbc.ml index 61e6b0b..05dc39a 100644 --- a/lib/AstOfLlbc.ml +++ b/lib/AstOfLlbc.ml @@ -301,6 +301,7 @@ let typ_of_literal_ty (_env : env) (ty : Charon.Types.literal_type) : K.typ = match ty with | TBool -> K.TBool | TChar -> failwith "TODO: Char" + | TFloat _ -> failwith "TODO: Float" | TInteger k -> K.TInt (width_of_integer_type k) let rec typ_of_ty (env : env) (ty : Charon.Types.ty) : K.typ =