diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fda5e4b3a..5f8aa18bc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -54,14 +54,20 @@ jobs: if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true' runs-on: [self-hosted, linux, nix] steps: - - run: nix flake check -L github:aeneasverif/aeneas --override-input charon github:aeneasverif/charon/${{ github.sha }} + - run: | + nix flake check -L github:aeneasverif/aeneas \ + --override-input charon github:aeneasverif/charon/${{ github.sha }} \ + --override-input charon/rust-overlay github:oxalica/rust-overlay/master eurydice: needs: [check_if_skip_duplicate_job, nix] if: needs.check_if_skip_duplicate_job.outputs.should_skip != 'true' runs-on: [self-hosted, linux, nix] steps: - - run: nix flake check -L github:aeneasverif/eurydice --override-input charon github:aeneasverif/charon/${{ github.sha }} + - run: | + nix flake check -L github:aeneasverif/eurydice \ + --override-input charon github:aeneasverif/charon/${{ github.sha }} \ + --override-input charon/rust-overlay github:oxalica/rust-overlay/master kyber: needs: [check_if_skip_duplicate_job, eurydice] diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 1b5b7c42d..4ae79100f 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -4,9 +4,9 @@ version = 3 [[package]] name = "addr2line" -version = "0.21.0" +version = "0.22.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8a30b2e23b9e17a9f90641c7ab1549cd9b44f296d3ccbf309d2863cfe398a0cb" +checksum = "6e4503c46a5c0c7844e948c9a4d6acd9f50cccb4de1c48eb9e291ea17470c678" dependencies = [ "gimli", ] @@ -19,9 +19,9 @@ checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" [[package]] name = "ahash" -version = "0.7.7" +version = "0.7.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a824f2aa7e75a0c98c5a504fceb80649e9c35265d44525b5f94de4771a395cd" +checksum = "891477e0c6a8957309ee5c45a6368af3ae14bb510732d2684ffa19af310920f9" dependencies = [ "getrandom", "once_cell", @@ -30,18 +30,18 @@ dependencies = [ [[package]] name = "aho-corasick" -version = "1.1.2" +version = "1.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2969dcb958b36655471fc61f7e416fa76033bdd4bfed0678d8fee1e2d07a1f0" +checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916" dependencies = [ "memchr", ] [[package]] name = "anyhow" -version = "1.0.81" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0952808a6c2afd1aa8947271f3a60f1a6763c7b912d210184c5149b5cf147247" +checksum = "b3d1d046238990b9cf5bcde22a3fb3584ee5cf65fb2765f454ed428c7a0063da" [[package]] name = "arrayvec" @@ -69,22 +69,22 @@ version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" dependencies = [ - "hermit-abi 0.1.19", + "hermit-abi", "libc", "winapi", ] [[package]] name = "autocfg" -version = "1.1.0" +version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" +checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" [[package]] name = "backtrace" -version = "0.3.69" +version = "0.3.73" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2089b7e3f35b9dd2d0ed921ead4f6d318c27680d4a5bd167b3ee120edb105837" +checksum = "5cc23269a4f8976d0a4d2e7109211a419fe30e8d88d677cd60b6bc79c5732e0a" dependencies = [ "addr2line", "cc", @@ -103,9 +103,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.4.1" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07" +checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" [[package]] name = "bitmaps" @@ -129,9 +129,9 @@ dependencies = [ [[package]] name = "bstr" -version = "1.8.0" +version = "1.9.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "542f33a8835a0884b006a0c3df3dadd99c0c3f296ed26c2fdc8028e01ad6230c" +checksum = "05efc5cfd9110c8416e471df0e96702d58690178e206e61b7173706673c93706" dependencies = [ "memchr", "serde", @@ -139,18 +139,15 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.14.0" +version = "3.16.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7f30e7476521f6f8af1a1c4c0b8cc94f0bee37d91763d0ca2665f299b6cd8aec" +checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c" [[package]] name = "cc" -version = "1.0.83" +version = "1.0.101" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" -dependencies = [ - "libc", -] +checksum = "ac367972e516d45567c7eafc73d24e1c193dcf200a8d94e9db7b3d38b349572d" [[package]] name = "cfg-if" @@ -245,11 +242,10 @@ dependencies = [ [[package]] name = "colored" -version = "2.0.4" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2674ec482fbc38012cf31e6c42ba0177b431a0cb6f15fe40efa5aab1bda516f6" +checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" dependencies = [ - "is-terminal", "lazy_static", "windows-sys 0.48.0", ] @@ -279,9 +275,9 @@ checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" [[package]] name = "crossbeam-channel" -version = "0.5.12" +version = "0.5.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ab3db02a9c5b5121e1e42fbdb1aeb65f5e02624cc58c43f2884c6ccac0b82f95" +checksum = "33480d6946193aa8033910124896ca395333cae7e2d1113d1fef6c3272217df2" dependencies = [ "crossbeam-utils", ] @@ -307,9 +303,9 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.19" +version = "0.8.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "248e3bacc7dc6baa3b21e405ee045c3047101a49145e7e9eca583ab4c2ca5345" +checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80" [[package]] name = "derivative" @@ -358,15 +354,15 @@ checksum = "fea41bba32d969b513997752735605054bc0dfa92b4c56bf1189f2e174be7a10" [[package]] name = "dyn-clone" -version = "1.0.16" +version = "1.0.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "545b22097d44f8a9581187cdf93de7a71e4722bf51200cfaba810865b49a495d" +checksum = "0d6ef0072f8a535281e4876be788938b528e9a1d43900b82c2569af7da799125" [[package]] name = "either" -version = "1.9.0" +version = "1.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a26ae43d7bcc3b814de94796a5e736d4029efb0ee900c12e2d54c993ad1a1e07" +checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" [[package]] name = "env_logger" @@ -389,9 +385,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" [[package]] name = "errno" -version = "0.3.8" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a258e46cdc063eb8519c00b9fc845fc47bcfca4130e2f08e88665ceda8474245" +checksum = "534c5cf6194dfab3db3242765c03bbe257cf92f22b38f6bc0c58d59108a820ba" dependencies = [ "libc", "windows-sys 0.52.0", @@ -428,9 +424,9 @@ dependencies = [ [[package]] name = "fastrand" -version = "2.0.2" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "658bd65b1cf4c852a3cc96f18a8ce7b5640f6b703f905c7d74532294c2a63984" +checksum = "9fc0510504f03c51ada170672ac806f1f105a88aa97a5281117e1ddc3368e51a" [[package]] name = "fixedbitset" @@ -440,9 +436,9 @@ checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" [[package]] name = "getrandom" -version = "0.2.11" +version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe9006bed769170c11f845cf00c7c1e9092aeb3f268e007c3e760ac68008070f" +checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" dependencies = [ "cfg-if", "libc", @@ -451,9 +447,9 @@ dependencies = [ [[package]] name = "gimli" -version = "0.28.1" +version = "0.29.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4271d37baee1b8c7e4b708028c57d816cf9d2434acb33a549475f78c181f6253" +checksum = "40ecd4077b5ae9fd2e9e169b102c6c330d0605168eb0e8bf79952b256dbefffd" [[package]] name = "globset" @@ -462,10 +458,10 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "57da3b9b5b85bd66f31093f8c408b90a74431672542466497dcbdfdc02034be1" dependencies = [ "aho-corasick", - "bstr 1.8.0", + "bstr 1.9.1", "log", - "regex-automata 0.4.3", - "regex-syntax 0.8.2", + "regex-automata 0.4.7", + "regex-syntax 0.8.4", ] [[package]] @@ -485,9 +481,9 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" [[package]] name = "hashbrown" -version = "0.14.3" +version = "0.14.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604" +checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" [[package]] name = "hashlink" @@ -501,7 +497,7 @@ dependencies = [ [[package]] name = "hax-adt-into" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#1fc4a032540111eb716b0cbc306899f397f443cf" +source = "git+https://github.com/hacspec/hax?branch=main#c711b19bf9f13ff64e8a08cf323194cba94bd2a0" dependencies = [ "itertools 0.11.0", "proc-macro2", @@ -512,7 +508,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#1fc4a032540111eb716b0cbc306899f397f443cf" +source = "git+https://github.com/hacspec/hax?branch=main#c711b19bf9f13ff64e8a08cf323194cba94bd2a0" dependencies = [ "extension-traits", "hax-adt-into", @@ -529,7 +525,7 @@ dependencies = [ [[package]] name = "hax-frontend-exporter-options" version = "0.1.0-pre.1" -source = "git+https://github.com/hacspec/hax?branch=main#1fc4a032540111eb716b0cbc306899f397f443cf" +source = "git+https://github.com/hacspec/hax?branch=main#c711b19bf9f13ff64e8a08cf323194cba94bd2a0" dependencies = [ "schemars", "serde", @@ -560,12 +556,6 @@ dependencies = [ "libc", ] -[[package]] -name = "hermit-abi" -version = "0.3.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d77f7ec81a6d05a3abb01ab6eb7590f6083d08449fe5a1c8b1e620283546ccb7" - [[package]] name = "home" version = "0.5.9" @@ -591,7 +581,7 @@ dependencies = [ "globset", "log", "memchr", - "regex-automata 0.4.3", + "regex-automata 0.4.7", "same-file", "walkdir", "winapi-util", @@ -632,12 +622,12 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.1.0" +version = "2.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d530e1a18b1cb4c484e6e34556a0d948706958449fca0cab753d649f2bce3d1f" +checksum = "168fb715dda47215e360912c096649d23d58bf392ac62f73919e831745e40f26" dependencies = [ "equivalent", - "hashbrown 0.14.3", + "hashbrown 0.14.5", ] [[package]] @@ -648,24 +638,13 @@ checksum = "b248f5224d1d606005e02c97f5aa4e88eeb230488bcc03bc9ca4d7991399f2b5" [[package]] name = "instant" -version = "0.1.12" +version = "0.1.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" +checksum = "e0242819d153cba4b4b05a5a8f2a7e9bbf97b6055b2a002b395c96b5ff3c0222" dependencies = [ "cfg-if", ] -[[package]] -name = "is-terminal" -version = "0.4.9" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" -dependencies = [ - "hermit-abi 0.3.3", - "rustix", - "windows-sys 0.48.0", -] - [[package]] name = "itertools" version = "0.10.5" @@ -686,21 +665,21 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.9" +version = "1.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" +checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "lazy_static" -version = "1.4.0" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" +checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.153" +version = "0.2.155" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c198f91728a82281a64e1f4f9eeb25d82cb32a5de251c6bd1b5154d63a8e7bd" +checksum = "97b3888a4aecf77e811145cadf6eef5901f4782c53886191b2f693f24761847c" [[package]] name = "libtest-mimic" @@ -731,15 +710,15 @@ dependencies = [ [[package]] name = "linux-raw-sys" -version = "0.4.12" +version = "0.4.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4cd1a83af159aa67994778be9070f0ae1bd732942279cabb14f86f986a21456" +checksum = "78b3ae25bc7c8c38cec158d1f2757ee79e9b3740fbc7ccf0e59e4b08d793fa89" [[package]] name = "lock_api" -version = "0.4.11" +version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3c168f8615b12bc01f9c17e2eb0cc07dcae1940121185446edc3744920e8ef45" +checksum = "07af8b9cdd281b7915f413fa73f29ebd5d55d0d3f0155584dade1ff18cea1b17" dependencies = [ "autocfg", "scopeguard", @@ -747,9 +726,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.20" +version = "0.4.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f" +checksum = "90ed8c1e510134f979dbc4f070f87d4313098b704861a105fe34231c70a3901c" [[package]] name = "macros" @@ -771,15 +750,15 @@ dependencies = [ [[package]] name = "memchr" -version = "2.6.4" +version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f665ee40bc4a3c5590afb1e9677db74a508659dfd71e126420da8274909a0167" +checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" [[package]] name = "miniz_oxide" -version = "0.7.1" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e7810e0be55b428ada41041c41f32c9f1a42817901b4ccf45fa3d4b6561e74c7" +checksum = "b8a240ddb74feaf34a79a7add65a741f3167852fba007066dcac1ca548d89c08" dependencies = [ "adler", ] @@ -811,18 +790,18 @@ dependencies = [ [[package]] name = "object" -version = "0.32.1" +version = "0.36.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9cf5f9dd3933bd50a9e1f149ec995f39ae2c496d31fd772c1fd45ebc27e902b0" +checksum = "576dfe1fc8f9df304abb159d767a29d0476f7750fbf8aa7ad07816004a207434" dependencies = [ "memchr", ] [[package]] name = "once_cell" -version = "1.18.0" +version = "1.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" +checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" [[package]] name = "os_str_bytes" @@ -856,32 +835,32 @@ dependencies = [ "cfg-if", "instant", "libc", - "redox_syscall 0.2.16", + "redox_syscall", "smallvec", "winapi", ] [[package]] name = "paste" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de3145af08024dea9fa9914f381a17b8fc6034dfb00f3a84013f7ff43f29ed4c" +checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" [[package]] name = "petgraph" -version = "0.6.4" +version = "0.6.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e1d3afd2628e69da2be385eb6f2fd57c8ac7977ceeff6dc166ff1657b0e386a9" +checksum = "b4c5cc86750666a3ed20bdaf5ca2a0344f9c67674cae0515bec2da16fbaa47db" dependencies = [ "fixedbitset", - "indexmap 2.1.0", + "indexmap 2.2.6", ] [[package]] name = "pin-project-lite" -version = "0.2.13" +version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8afb450f006bf6385ca15ef45d71d2288452bc3683ce2e2cacc0d18e4be60b58" +checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" [[package]] name = "predicates" @@ -946,9 +925,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.79" +version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e835ff2298f5721608eb1a980ecaee1aef2c132bf95ecc026a11b7bf3c01c02e" +checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" dependencies = [ "unicode-ident", ] @@ -964,9 +943,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.35" +version = "1.0.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "291ec9ab5efd934aaf503a6466c5d5251535d108ee747472c3977cc5acc868ef" +checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" dependencies = [ "proc-macro2", ] @@ -1015,25 +994,16 @@ dependencies = [ "bitflags 1.3.2", ] -[[package]] -name = "redox_syscall" -version = "0.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4722d768eff46b75989dd134e5c353f0d6296e5aaa3132e776cbdb56be7731aa" -dependencies = [ - "bitflags 1.3.2", -] - [[package]] name = "regex" -version = "1.10.2" +version = "1.10.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343" +checksum = "b91213439dad192326a0d7c6ee3955910425f441d7038e0d6933b0aec5c4517f" dependencies = [ "aho-corasick", "memchr", - "regex-automata 0.4.3", - "regex-syntax 0.8.2", + "regex-automata 0.4.7", + "regex-syntax 0.8.4", ] [[package]] @@ -1047,13 +1017,13 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.3" +version = "0.4.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5f804c7828047e88b2d32e2d7fe5a105da8ee3264f01902f796c8e067dc2483f" +checksum = "38caf58cc5ef2fed281f89292ef23f6365465ed9a41b7a7754eb4e26496c92df" dependencies = [ "aho-corasick", "memchr", - "regex-syntax 0.8.2", + "regex-syntax 0.8.4", ] [[package]] @@ -1064,15 +1034,15 @@ checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" [[package]] name = "regex-syntax" -version = "0.8.2" +version = "0.8.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f" +checksum = "7a66a03ae7c801facd77a29370b4faec201768915ac14a721ba36f20bc9c209b" [[package]] name = "rustc-demangle" -version = "0.1.23" +version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" +checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" [[package]] name = "rustc_version" @@ -1085,11 +1055,11 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.32" +version = "0.38.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "65e04861e65f21776e67888bfbea442b3642beaa0138fdb1dd7a84a52dffdb89" +checksum = "70dc5ec042f7a43c4a73241207cecc9873a06d45debb38b329f8541d85c2730f" dependencies = [ - "bitflags 2.4.1", + "bitflags 2.6.0", "errno", "libc", "linux-raw-sys", @@ -1098,9 +1068,9 @@ dependencies = [ [[package]] name = "ryu" -version = "1.0.15" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" +checksum = "f3cb5ba0dc43242ce17de99c180e96db90b235b8a9fdc9543c96d2209116bd9f" [[package]] name = "same-file" @@ -1113,9 +1083,9 @@ dependencies = [ [[package]] name = "schemars" -version = "0.8.16" +version = "0.8.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "45a28f4c49489add4ce10783f7911893516f15afe45d015608d41faca6bc4d29" +checksum = "09c024468a378b7e36765cd36702b7a90cc3cba11654f6685c8f233408e89e92" dependencies = [ "dyn-clone", "schemars_derive", @@ -1125,14 +1095,14 @@ dependencies = [ [[package]] name = "schemars_derive" -version = "0.8.16" +version = "0.8.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c767fd6fa65d9ccf9cf026122c1b555f2ef9a4f0cea69da4d7dbc3e258d30967" +checksum = "b1eee588578aff73f856ab961cd2f79e36bc45d7ded33a7562adba4667aecc0e" dependencies = [ "proc-macro2", "quote", "serde_derive_internals", - "syn 1.0.109", + "syn 2.0.68", ] [[package]] @@ -1158,40 +1128,40 @@ checksum = "388a1df253eca08550bef6c72392cfe7c30914bf41df5269b68cbd6ff8f570a3" [[package]] name = "serde" -version = "1.0.197" +version = "1.0.203" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fb1c873e1b9b056a4dc4c0c198b24c3ffa059243875552b2bd0933b1aee4ce2" +checksum = "7253ab4de971e72fb7be983802300c30b5a7f0c2e56fab8abfc6a214307c0094" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.197" +version = "1.0.203" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7eb0b34b42edc17f6b7cac84a52a1c5f0e1bb2227e997ca9011ea3dd34e8610b" +checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba" dependencies = [ "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.68", ] [[package]] name = "serde_derive_internals" -version = "0.26.0" +version = "0.29.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85bf8229e7920a9f636479437026331ce11aa132b4dde37d121944a44d6e5f3c" +checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711" dependencies = [ "proc-macro2", "quote", - "syn 1.0.109", + "syn 2.0.68", ] [[package]] name = "serde_json" -version = "1.0.108" +version = "1.0.118" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3d1c7e3eac408d115102c4c24ad393e0821bb3a5df4d506a80f85f7a742a526b" +checksum = "d947f6b3163d8857ea16c4fa0dd4840d52f3041039a85decd46867eb1abef2e4" dependencies = [ "itoa", "ryu", @@ -1256,9 +1226,9 @@ dependencies = [ [[package]] name = "smallvec" -version = "1.11.2" +version = "1.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4dccd0940a2dcdf68d092b8cbab7dc0ad8fa938bf95787e1b916b0e3d0e8e970" +checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" [[package]] name = "snapbox" @@ -1275,9 +1245,9 @@ dependencies = [ [[package]] name = "snapbox-macros" -version = "0.3.8" +version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e1c4b838b05d15ab22754068cb73500b2f3b07bf09d310e15b27f88160f1de40" +checksum = "b1f4c14672714436c09254801c934b203196a51182a5107fb76591c7cc56424d" [[package]] name = "stacker" @@ -1311,9 +1281,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.58" +version = "2.0.68" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44cfb93f38070beee36b3fef7d4f5a16f27751d94b187b666a5cc5e9b0d30687" +checksum = "901fa70d88b9d6c98022e23b4136f9f3e54e4662c3bc1bd1d84a42a9a0f0c1e9" dependencies = [ "proc-macro2", "quote", @@ -1328,22 +1298,21 @@ checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60" [[package]] name = "tempfile" -version = "3.9.0" +version = "3.10.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "01ce4141aa927a6d1bd34a041795abd0db1cccba5d5f24b009f694bdf3a1f3fa" +checksum = "85b77fafb263dd9d05cbeac119526425676db3784113aa9295c88498cbf8bff1" dependencies = [ "cfg-if", "fastrand", - "redox_syscall 0.4.1", "rustix", "windows-sys 0.52.0", ] [[package]] name = "termcolor" -version = "1.4.0" +version = "1.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ff1bc3d3f05aff0403e8ac0d92ced918ec05b666a43f83297ccef5bea8a3d449" +checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" dependencies = [ "winapi-util", ] @@ -1372,9 +1341,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.13" +version = "0.8.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a4e43f8cc456c9704c851ae29c67e17ef65d2c30017c17a9765b89c382dc8bba" +checksum = "6f49eb2ab21d2f26bd6db7bf383edc527a7ebaee412d17af4d40fdccd442f335" dependencies = [ "serde", "serde_spanned", @@ -1393,11 +1362,11 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.22.13" +version = "0.22.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c127785850e8c20836d49732ae6abfa47616e60bf9d9f57c43c250361a9db96c" +checksum = "f21c7aaf97f1bd9ca9d4f9e73b0a6c74bd5afef56f2bc931943a6e1c37e04e38" dependencies = [ - "indexmap 2.1.0", + "indexmap 2.2.6", "serde", "serde_spanned", "toml_datetime", @@ -1423,7 +1392,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.58", + "syn 2.0.68", ] [[package]] @@ -1508,9 +1477,9 @@ checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" [[package]] name = "unicode-segmentation" -version = "1.10.1" +version = "1.11.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1dd624098567895118886609431a7c3b8f516e41d30e0643f03d94592a147e36" +checksum = "d4c87d22b6e3f4a18d4d40ef354e97c90fcb14dd91d7dc0aa9d8a1172ebf7202" [[package]] name = "valuable" @@ -1535,9 +1504,9 @@ dependencies = [ [[package]] name = "walkdir" -version = "2.4.0" +version = "2.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d71d857dc86794ca4c280d616f7da00d2dbfd8cd788846559a6813e6aa4b54ee" +checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b" dependencies = [ "same-file", "winapi-util", @@ -1579,11 +1548,11 @@ checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" [[package]] name = "winapi-util" -version = "0.1.6" +version = "0.1.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f29e6f9198ba0d26b4c9f07dbe6f9ed633e1f3d5b8b414090084349e46a52596" +checksum = "4d4cc384e1e73b93bafa6fb4f1df8c41695c8a91cf9c4c64358067d15a7b6c6b" dependencies = [ - "winapi", + "windows-sys 0.52.0", ] [[package]] @@ -1607,7 +1576,7 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets 0.52.0", + "windows-targets 0.52.5", ] [[package]] @@ -1627,17 +1596,18 @@ dependencies = [ [[package]] name = "windows-targets" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8a18201040b24831fbb9e4eb208f8892e1f50a37feb53cc7ff887feb8f50e7cd" +checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb" dependencies = [ - "windows_aarch64_gnullvm 0.52.0", - "windows_aarch64_msvc 0.52.0", - "windows_i686_gnu 0.52.0", - "windows_i686_msvc 0.52.0", - "windows_x86_64_gnu 0.52.0", - "windows_x86_64_gnullvm 0.52.0", - "windows_x86_64_msvc 0.52.0", + "windows_aarch64_gnullvm 0.52.5", + "windows_aarch64_msvc 0.52.5", + "windows_i686_gnu 0.52.5", + "windows_i686_gnullvm", + "windows_i686_msvc 0.52.5", + "windows_x86_64_gnu 0.52.5", + "windows_x86_64_gnullvm 0.52.5", + "windows_x86_64_msvc 0.52.5", ] [[package]] @@ -1648,9 +1618,9 @@ checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" [[package]] name = "windows_aarch64_gnullvm" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea" +checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263" [[package]] name = "windows_aarch64_msvc" @@ -1660,9 +1630,9 @@ checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" [[package]] name = "windows_aarch64_msvc" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef" +checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6" [[package]] name = "windows_i686_gnu" @@ -1672,9 +1642,15 @@ checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" [[package]] name = "windows_i686_gnu" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313" +checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9" [[package]] name = "windows_i686_msvc" @@ -1684,9 +1660,9 @@ checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" [[package]] name = "windows_i686_msvc" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a" +checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf" [[package]] name = "windows_x86_64_gnu" @@ -1696,9 +1672,9 @@ checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" [[package]] name = "windows_x86_64_gnu" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd" +checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9" [[package]] name = "windows_x86_64_gnullvm" @@ -1708,9 +1684,9 @@ checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" [[package]] name = "windows_x86_64_gnullvm" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e" +checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596" [[package]] name = "windows_x86_64_msvc" @@ -1720,15 +1696,15 @@ checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" [[package]] name = "windows_x86_64_msvc" -version = "0.52.0" +version = "0.52.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04" +checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0" [[package]] name = "winnow" -version = "0.6.8" +version = "0.6.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3c52e9c97a68071b23e836c9380edae937f17b9c4667bd021973efc689f618d" +checksum = "59b5e5f6c299a3c7890b876a2a587f3115162487e704907d9b6cd29473052ba1" dependencies = [ "memchr", ] diff --git a/charon/src/ast/meta_utils.rs b/charon/src/ast/meta_utils.rs index 5ff4f523f..e723e77eb 100644 --- a/charon/src/ast/meta_utils.rs +++ b/charon/src/ast/meta_utils.rs @@ -3,7 +3,7 @@ use crate::meta::*; use hax_frontend_exporter as hax; use rustc_hir::def_id::DefId; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; +use rustc_span::source_map::SourceMap; use std::cmp::Ordering; use std::iter::Iterator; use std::path::Component; @@ -133,11 +133,7 @@ pub fn convert_loc(loc: hax::Loc) -> Loc { } // TODO: remove? -pub fn span_to_string(sess: &Session, span: rustc_span::Span) -> String { - // Retrieve the source map, which contains information about the source file: - // we need it to be able to interpret the span. - let source_map = sess.source_map(); - +pub fn span_to_string(source_map: &SourceMap, span: rustc_span::Span) -> String { // Convert the span to lines let (beg, end) = source_map.is_valid_span(span).unwrap(); diff --git a/charon/src/ast/names_utils.rs b/charon/src/ast/names_utils.rs index ae755ed80..531820cd9 100644 --- a/charon/src/ast/names_utils.rs +++ b/charon/src/ast/names_utils.rs @@ -250,7 +250,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { kind, })); } - DefPathData::ImplTrait => { + DefPathData::OpaqueTy => { // TODO: do nothing for now } DefPathData::MacroNs(symbol) => { @@ -263,7 +263,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { // instance to filter opaque modules. name.push(PathElem::Ident(symbol.to_string(), disambiguator)); } - DefPathData::ClosureExpr => { + DefPathData::Closure => { // TODO: this is not very satisfactory, but on the other hand // we should be able to extract closures in local let-bindings // (i.e., we shouldn't have to introduce top-level let-bindings). diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index 51e4adaba..f6c5ec39a 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -9,7 +9,6 @@ use regex::Regex; use rustc_driver::{Callbacks, Compilation}; use rustc_interface::{interface::Compiler, Queries}; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; use std::fmt; use std::ops::Deref; use std::panic::{self, AssertUnwindSafe}; @@ -101,7 +100,7 @@ impl Callbacks for CharonCallbacks { /// possible (i.e., after parsing). See [charon_lib::get_mir]. fn after_crate_root_parsing<'tcx>( &mut self, - c: &Compiler, + _c: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { // Set up our own `DefId` debug routine. @@ -113,8 +112,7 @@ impl Callbacks for CharonCallbacks { .unwrap() .get_mut() .enter(|tcx| { - let session = c.session(); - let crate_data = translate(session, tcx, self)?; + let crate_data = translate(tcx, self)?; self.crate_data = Some(crate_data); Ok::<(), ()>(()) }) @@ -208,11 +206,7 @@ pub fn get_args_crate_index>(args: &[T]) -> Option /// /// This function is a callback function for the Rust compiler. #[allow(clippy::result_unit_err)] -pub fn translate( - sess: &Session, - tcx: TyCtxt, - internal: &mut CharonCallbacks, -) -> Result { +pub fn translate(tcx: TyCtxt, internal: &mut CharonCallbacks) -> Result { trace!(); let options = &internal.options; @@ -246,11 +240,10 @@ pub fn translate( // # Translate the declarations in the crate. // We translate the declarations in an ad-hoc order, and do not group // the mutually recursive groups - we do this in the next step. - let mut ctx = - match translate_crate_to_ullbc::translate(crate_name, options, sess, tcx, mir_level) { - Ok(ctx) => ctx, - Err(_) => return Err(()), - }; + let mut ctx = match translate_crate_to_ullbc::translate(crate_name, options, tcx, mir_level) { + Ok(ctx) => ctx, + Err(_) => return Err(()), + }; if options.print_ullbc { info!("# ULLBC after translation from MIR:\n\n{ctx}\n"); diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs index 14add4a86..ec69ac16e 100644 --- a/charon/src/bin/charon-driver/main.rs +++ b/charon/src/bin/charon-driver/main.rs @@ -6,7 +6,6 @@ extern crate rustc_driver; extern crate rustc_hir; extern crate rustc_interface; extern crate rustc_middle; -extern crate rustc_session; extern crate rustc_span; #[macro_use] diff --git a/charon/src/bin/charon/main.rs b/charon/src/bin/charon/main.rs index 77a48bb6b..4b7ffa031 100644 --- a/charon/src/bin/charon/main.rs +++ b/charon/src/bin/charon/main.rs @@ -30,8 +30,6 @@ //! deserialize them later and use them to guide the extraction in the //! callbacks. -#![cfg_attr(feature = "deny-warnings", deny(warnings))] - // Don't link with the `charon_lib` crate so that the `charon` binary doesn't have to dynamically // link to `librustc_driver.so` etc. #[path = "../../cli_options.rs"] diff --git a/charon/src/deps_errors.rs b/charon/src/deps_errors.rs index 3ee2d1ef7..04cb7e439 100644 --- a/charon/src/deps_errors.rs +++ b/charon/src/deps_errors.rs @@ -1,5 +1,6 @@ //! Utilities to generate error reports about the external dependencies. use crate::translate_ctx::*; +use macros::VariantIndexArity; use petgraph::algo::dijkstra::dijkstra; use petgraph::graphmap::DiGraphMap; use rustc_error_messages::MultiSpan; @@ -7,13 +8,34 @@ use rustc_hir::def_id::DefId; use rustc_span::Span; /// For error reporting -#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)] +#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, VariantIndexArity)] enum Node { External(DefId), /// We use the span information only for local references Local(DefId, Span), } +impl Node { + /// Value with which we order `Node`s. + fn sort_key(&self) -> impl Ord { + let (variant_index, _) = self.variant_index_arity(); + let (Self::External(def_id) | Self::Local(def_id, _)) = self; + (variant_index, def_id.index, def_id.krate) + } +} + +/// Manual impls because `DefId` is not orderable. +impl PartialOrd for Node { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} +impl Ord for Node { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.sort_key().cmp(&other.sort_key()) + } +} + struct Graph { dgraph: DiGraphMap, } diff --git a/charon/src/lib.rs b/charon/src/lib.rs index 35a862b97..4234a6a10 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -15,21 +15,22 @@ #![feature(box_patterns)] // For rustdoc: prevents overflows #![recursion_limit = "256"] -#![feature(trait_alias)] -#![feature(let_chains)] #![feature(if_let_guard)] -#![feature(iter_array_chunks)] #![feature(impl_trait_in_assoc_type)] +#![feature(iter_array_chunks)] #![feature(iterator_try_collect)] +#![feature(let_chains)] +#![feature(lint_reasons)] +#![feature(trait_alias)] extern crate rustc_ast; extern crate rustc_ast_pretty; extern crate rustc_attr; extern crate rustc_error_messages; +extern crate rustc_errors; extern crate rustc_hir; extern crate rustc_index; extern crate rustc_middle; -extern crate rustc_session; extern crate rustc_span; extern crate rustc_target; diff --git a/charon/src/translate/translate_crate_to_ullbc.rs b/charon/src/translate/translate_crate_to_ullbc.rs index 05940e32d..1ede5bb6e 100644 --- a/charon/src/translate/translate_crate_to_ullbc.rs +++ b/charon/src/translate/translate_crate_to_ullbc.rs @@ -9,7 +9,6 @@ use hax_frontend_exporter::SInto; use rustc_hir::def_id::DefId; use rustc_hir::{ForeignItemKind, ImplItemKind, Item, ItemKind}; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; use std::collections::{HashMap, HashSet}; impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { @@ -102,8 +101,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { trace!("impl"); // Sanity checks // TODO: make proper error messages - use rustc_hir::{Defaultness, ImplPolarity, Unsafety}; - assert!(impl_block.unsafety == Unsafety::Normal); + use rustc_hir::{Defaultness, ImplPolarity, Safety}; + assert!(impl_block.safety == Safety::Safe); // About polarity: // [https://doc.rust-lang.org/beta/unstable-book/language-features/negative-impls.html] // Not sure about what I should do about it. Should I do anything, actually? @@ -342,10 +341,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { pub fn translate<'tcx, 'ctx>( crate_name: String, options: &CliOpts, - session: &'ctx Session, tcx: TyCtxt<'tcx>, mir_level: MirLevel, -) -> Result, Error> { +) -> Result, Error> { let hax_state = hax::state::State::new( tcx, hax::options::Options { @@ -364,7 +362,7 @@ pub fn translate<'tcx, 'ctx>( errors: ErrorCtx { continue_on_failure: !options.abort_on_error, errors_as_warnings: options.errors_as_warnings, - session, + dcx: tcx.dcx(), decls_with_errors: HashSet::new(), ignored_failed_decls: HashSet::new(), dep_sources: HashMap::new(), @@ -397,10 +395,8 @@ pub fn translate<'tcx, 'ctx>( let hir = tcx.hir(); for item_id in hir.root_module().item_ids { let item_id = item_id.hir_id(); - let node = hir.find(item_id).unwrap(); - let item = match node { - rustc_hir::Node::Item(item) => item, - _ => unreachable!(), + let rustc_hir::Node::Item(item) = tcx.hir_node(item_id) else { + unreachable!() }; ctx.register_local_hir_item(true, item)?; } diff --git a/charon/src/translate/translate_ctx.rs b/charon/src/translate/translate_ctx.rs index 64af9ea66..d7deec2a0 100644 --- a/charon/src/translate/translate_ctx.rs +++ b/charon/src/translate/translate_ctx.rs @@ -19,12 +19,12 @@ use hax_frontend_exporter::SInto; use linked_hash_set::LinkedHashSet; use macros::{EnumAsGetters, EnumIsA, VariantIndexArity, VariantName}; use rustc_error_messages::MultiSpan; +use rustc_errors::DiagCtxtHandle; use rustc_hir::def_id::DefId; use rustc_hir::Node as HirNode; use rustc_middle::ty::TyCtxt; -use rustc_session::Session; use serde::{Deserialize, Serialize}; -use std::cmp::{Ord, Ordering, PartialOrd}; +use std::cmp::{Ord, PartialOrd}; use std::collections::{BTreeMap, HashMap, HashSet, VecDeque}; use std::fmt; @@ -71,12 +71,31 @@ pub(crate) use error_assert; /// dependencies, especially if some external dependencies don't extract: /// we use this information to tell the user what is the code which /// (transitively) lead to the extraction of those problematic dependencies. -#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq, PartialOrd, Ord)] +#[derive(Debug, Clone, Copy, Hash, PartialEq, Eq)] pub struct DepSource { pub src_id: DefId, pub span: rustc_span::Span, } +impl DepSource { + /// Value with which we order `DepSource`s. + fn sort_key(&self) -> impl Ord { + (self.src_id.index, self.src_id.krate) + } +} + +/// Manual impls because `DefId` is not orderable. +impl PartialOrd for DepSource { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} +impl Ord for DepSource { + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.sort_key().cmp(&other.sort_key()) + } +} + impl DepSource { pub(crate) fn make(src_id: DefId, span: rustc_span::Span) -> Option { Some(DepSource { src_id, span }) @@ -174,23 +193,24 @@ impl OrdRustId { } } -impl PartialOrd for OrdRustId { - fn partial_cmp(&self, other: &OrdRustId) -> Option { - let (vid0, _) = self.variant_index_arity(); - let (vid1, _) = other.variant_index_arity(); - if vid0 != vid1 { - Option::Some(vid0.cmp(&vid1)) - } else { - let id0 = self.get_id(); - let id1 = other.get_id(); - Some(id0.cmp(&id1)) - } +impl OrdRustId { + /// Value with which we order values. + fn sort_key(&self) -> impl Ord { + let (variant_index, _) = self.variant_index_arity(); + let def_id = self.get_id(); + (variant_index, def_id.index, def_id.krate) } } +/// Manual impls because `DefId` is not orderable. +impl PartialOrd for OrdRustId { + fn partial_cmp(&self, other: &Self) -> Option { + Some(self.cmp(other)) + } +} impl Ord for OrdRustId { - fn cmp(&self, other: &OrdRustId) -> Ordering { - self.partial_cmp(other).unwrap() + fn cmp(&self, other: &Self) -> std::cmp::Ordering { + self.sort_key().cmp(&other.sort_key()) } } @@ -251,7 +271,7 @@ pub struct ErrorCtx<'ctx> { pub errors_as_warnings: bool, /// The compiler session, used for displaying errors. - pub session: &'ctx Session, + pub dcx: DiagCtxtHandle<'ctx>, /// The ids of the declarations for which extraction we encountered errors. pub decls_with_errors: HashSet, /// The ids of the declarations we completely failed to extract and had to ignore. @@ -389,9 +409,9 @@ impl ErrorCtx<'_> { pub(crate) fn span_err_no_register>(&self, span: S, msg: &str) { let msg = msg.to_string(); if self.errors_as_warnings { - self.session.span_warn(span, msg); + self.dcx.span_warn(span, msg); } else { - self.session.span_err(span, msg); + self.dcx.span_err(span, msg); } } @@ -596,9 +616,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// Returns the attributes (`#[...]`) of this node. pub(crate) fn node_attributes(&self, id: DefId) -> &[rustc_ast::Attribute] { - let hir = self.tcx.hir(); id.as_local() - .map(|local_def_id| hir.attrs(hir.local_def_id_to_hir_id(local_def_id))) + .map(|local_def_id| { + self.tcx + .hir() + .attrs(self.tcx.local_def_id_to_hir_id(local_def_id)) + }) .unwrap_or_default() } @@ -684,7 +707,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { | Ctor { .. } | ExternCrate | ForeignMod - | Coroutine | GlobalAsm | InlineConst | LifetimeParam @@ -702,10 +724,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { /// Whether this item is in an `extern { .. }` block, in which case it has no body. pub(crate) fn id_is_extern_item(&mut self, id: DefId) -> bool { - id.as_local().is_some_and(|local_def_id| { - let node = self.tcx.hir().find_by_def_id(local_def_id); - matches!(node, Some(HirNode::ForeignItem(_))) - }) + self.tcx + .hir() + .get_if_local(id) + .is_some_and(|node| matches!(node, HirNode::ForeignItem(_))) } pub(crate) fn is_opaque_name(&self, name: &Name) -> bool { diff --git a/charon/src/translate/translate_functions_to_ullbc.rs b/charon/src/translate/translate_functions_to_ullbc.rs index 2467a0b24..1fcf70ef3 100644 --- a/charon/src/translate/translate_functions_to_ullbc.rs +++ b/charon/src/translate/translate_functions_to_ullbc.rs @@ -55,7 +55,9 @@ fn translate_borrow_kind(borrow_kind: hax::BorrowKind) -> BorrowKind { hax::MutBorrowKind::TwoPhaseBorrow => BorrowKind::TwoPhaseMut, hax::MutBorrowKind::ClosureCapture => unimplemented!(), }, - hax::BorrowKind::Fake => BorrowKind::Shallow, + hax::BorrowKind::Fake(hax::FakeBorrowKind::Shallow) => BorrowKind::Shallow, + // This one is used only in deref patterns. + hax::BorrowKind::Fake(hax::FakeBorrowKind::Deep) => unimplemented!(), } } @@ -63,6 +65,7 @@ fn translate_unaryop_kind(binop: hax::UnOp) -> UnOp { match binop { hax::UnOp::Not => UnOp::Not, hax::UnOp::Neg => UnOp::Neg, + hax::UnOp::PtrMetadata => unimplemented!("Unop::PtrMetadata"), } } @@ -72,27 +75,33 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { span: rustc_span::Span, binop: hax::BinOp, ) -> Result { - match binop { - hax::BinOp::BitXor => Ok(BinOp::BitXor), - hax::BinOp::BitAnd => Ok(BinOp::BitAnd), - hax::BinOp::BitOr => Ok(BinOp::BitOr), - hax::BinOp::Eq => Ok(BinOp::Eq), - hax::BinOp::Lt => Ok(BinOp::Lt), - hax::BinOp::Le => Ok(BinOp::Le), - hax::BinOp::Ne => Ok(BinOp::Ne), - hax::BinOp::Ge => Ok(BinOp::Ge), - hax::BinOp::Gt => Ok(BinOp::Gt), - hax::BinOp::Div => Ok(BinOp::Div), - hax::BinOp::Rem => Ok(BinOp::Rem), - hax::BinOp::Add => Ok(BinOp::Add), - hax::BinOp::Sub => Ok(BinOp::Sub), - hax::BinOp::Mul => Ok(BinOp::Mul), - hax::BinOp::Shl => Ok(BinOp::Shl), - hax::BinOp::Shr => Ok(BinOp::Shr), + Ok(match binop { + hax::BinOp::BitXor => BinOp::BitXor, + hax::BinOp::BitAnd => BinOp::BitAnd, + hax::BinOp::BitOr => BinOp::BitOr, + hax::BinOp::Eq => BinOp::Eq, + hax::BinOp::Lt => BinOp::Lt, + hax::BinOp::Le => BinOp::Le, + hax::BinOp::Ne => BinOp::Ne, + hax::BinOp::Ge => BinOp::Ge, + hax::BinOp::Gt => BinOp::Gt, + hax::BinOp::Div => BinOp::Div, + hax::BinOp::Rem => BinOp::Rem, + hax::BinOp::Add => BinOp::Add, + hax::BinOp::Sub => BinOp::Sub, + hax::BinOp::Mul => BinOp::Mul, + hax::BinOp::AddWithOverflow => BinOp::CheckedAdd, + hax::BinOp::SubWithOverflow => BinOp::CheckedSub, + hax::BinOp::MulWithOverflow => BinOp::CheckedMul, + hax::BinOp::Shl => BinOp::Shl, + hax::BinOp::Shr => BinOp::Shr, + hax::BinOp::Cmp => { + error_or_panic!(self, span, "Unsupported binary operation: Cmp") + } hax::BinOp::Offset => { error_or_panic!(self, span, "Unsupported binary operation: offset") } - } + }) } pub(crate) fn get_item_kind( @@ -644,12 +653,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } ( hax::CastKind::PointerCoercion(hax::PointerCoercion::ClosureFnPointer( - unsafety, + safety, )), src_ty @ Ty::Arrow(..), tgt_ty @ Ty::Arrow(..), ) => { - assert!(*unsafety == hax::Unsafety::Normal); + assert!(*safety == hax::Safety::Safe); let src_ty = src_ty.clone(); let tgt_ty = tgt_ty.clone(); Ok(Rvalue::UnaryOp( @@ -686,21 +695,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { self.translate_operand(span, left)?, self.translate_operand(span, right)?, )), - hax::Rvalue::CheckedBinaryOp(binop, (left, right)) => { - let binop = match binop { - hax::BinOp::Add => BinOp::CheckedAdd, - hax::BinOp::Sub => BinOp::CheckedSub, - hax::BinOp::Mul => BinOp::CheckedMul, - _ => { - error_or_panic!(self, span, "Only Add, Sub and Mul are supported as checked binary operations, found {binop:?}"); - } - }; - Ok(Rvalue::BinaryOp( - binop, - self.translate_operand(span, left)?, - self.translate_operand(span, right)?, - )) - } hax::Rvalue::NullaryOp(nullop, _ty) => { trace!("NullOp: {:?}", nullop); // Nullary operations are very low-level and shouldn't be necessary @@ -824,7 +818,11 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { Ok(Rvalue::Aggregate(akind, operands_t)) } - hax::AggregateKind::Coroutine(_def_id, _subst, _movability) => { + hax::AggregateKind::RawPtr(..) => { + error_or_panic!(self, span, "Raw pointers are not supported"); + } + hax::AggregateKind::Coroutine(..) + | hax::AggregateKind::CoroutineClosure(..) => { error_or_panic!(self, span, "Coroutines are not supported"); } } @@ -852,7 +850,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { erase_regions: bool, def_id: &hax::DefId, substs: &Vec, - args: Option<&Vec>, + args: Option<&Vec>>, trait_refs: &Vec, trait_info: &Option, ) -> Result { @@ -869,7 +867,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // sometimes introduces very low-level functions, which we need to // catch early - in particular, before we start translating types and // arguments, because we won't be able to translate some of them. - if matches!(builtin_fun, Some(BuiltinFun::BoxFree)) { + let sfid = if matches!(builtin_fun, Some(BuiltinFun::BoxFree)) { assert!(!is_local); // This deallocates a box. @@ -892,7 +890,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Translate the first argument - note that we use a special // function to translate it: the operand should be of the form: // `move b.0`, and if it is the case it will return `move b` - let arg = &args[0]; + let arg = &args[0].node; let t_arg = self.translate_move_box_first_projector_operand(span, arg)?; Ok(vec![t_arg]) }) @@ -903,8 +901,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { func: FunIdOrTraitMethodRef::mk_assumed(AssumedFunId::BoxFree), generics: GenericArgs::new_from_types(vec![t_ty]), }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + SubstFunId { func, args } } else { // Retrieve the lists of used parameters, in case of non-local // definitions @@ -945,7 +942,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // Check if the function is considered primitive: primitive // functions benefit from special treatment. - if let Some(builtin_fun) = builtin_fun { + let func = if let Some(builtin_fun) = builtin_fun { // Primitive function. // // Note that there are subtleties with regards to the way types parameters @@ -992,22 +989,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } }; - let func = FnPtr { - func: FunIdOrTraitMethodRef::Fun(FunId::Assumed(aid)), - generics, - }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + FunIdOrTraitMethodRef::Fun(FunId::Assumed(aid)) } else { // Two cases depending on whether we call a trait method or not match trait_info { None => { // "Regular" function call let def_id = self.register_fun_decl_id(span, rust_id); - let func = FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id)); - let func = FnPtr { func, generics }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + FunIdOrTraitMethodRef::Fun(FunId::Regular(def_id)) } Some(trait_info) => { // Trait method @@ -1023,18 +1012,16 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let trait_method_fun_id = self.register_fun_decl_id(span, rust_id); let method_name = self.t_ctx.translate_trait_item_name(rust_id)?; - let func = FunIdOrTraitMethodRef::Trait( - impl_expr, - method_name, - trait_method_fun_id, - ); - let func = FnPtr { func, generics }; - let sfid = SubstFunId { func, args }; - Ok(SubstFunIdOrPanic::Fun(sfid)) + FunIdOrTraitMethodRef::Trait(impl_expr, method_name, trait_method_fun_id) } } + }; + SubstFunId { + func: FnPtr { func, generics }, + args, } - } + }; + Ok(SubstFunIdOrPanic::Fun(sfid)) } /// Translate a statement @@ -1308,7 +1295,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { span: rustc_span::Span, fun: &hax::FunOperand, generics: &Vec, - args: &Vec, + args: &Vec>, destination: &hax::Place, target: &Option, trait_refs: &Vec, @@ -1399,13 +1386,14 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { &mut self, span: rustc_span::Span, used_args: Option>, - args: &Vec, + args: &Vec>, ) -> Result, Error> { + let unspanned_args = args.iter().map(|x| &x.node); let args: Vec<&hax::Operand> = match used_args { - None => args.iter().collect(), + None => unspanned_args.collect(), Some(used_args) => { assert!(args.len() == used_args.len()); - args.iter() + unspanned_args .zip(used_args.into_iter()) .filter_map(|(param, used)| if used { Some(param) } else { None }) .collect() @@ -1514,7 +1502,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let tcx = self.t_ctx.tcx; let erase_regions = false; let span = self.t_ctx.tcx.def_span(def_id); - let is_closure = tcx.is_closure(def_id); + let is_closure = tcx.is_closure_like(def_id); let dep_src = DepSource::make(def_id, span); // The parameters (and in particular the lifetimes) are split between @@ -1569,10 +1557,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { trace!("closure.sig_as_fn_ptr_ty: {:?}", closure.sig_as_fn_ptr_ty()); trace!("closure.kind_ty: {:?}", closure.kind_ty()); - trace!( - "closure.print_as_impl_trait: {:?}", - closure.print_as_impl_trait() - ); // Sanity check: the parent subst only contains types and generics error_assert!( @@ -1621,9 +1605,9 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { // // Add the *late-bound* parameters (bound in the signature, can only be lifetimes) // - let is_unsafe = match signature.value.unsafety { - hax::Unsafety::Unsafe => true, - hax::Unsafety::Normal => false, + let is_unsafe = match signature.value.safety { + hax::Safety::Unsafe => true, + hax::Safety::Safe => false, }; let bvar_names = signature .bound_vars diff --git a/charon/src/translate/translate_predicates.rs b/charon/src/translate/translate_predicates.rs index df504353e..4e9feb534 100644 --- a/charon/src/translate/translate_predicates.rs +++ b/charon/src/translate/translate_predicates.rs @@ -58,7 +58,7 @@ impl NonLocalTraitClause { #[derive(Debug, Clone, EnumIsA, EnumAsGetters, EnumToGetters)] pub(crate) enum Predicate { - Trait(TraitClauseId), + Trait(#[expect(dead_code)] TraitClauseId), TypeOutlives(TypeOutlives), RegionOutlives(RegionOutlives), TraitType(TraitTypeConstraint), @@ -537,10 +537,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } PredicateKind::AliasRelate(..) | PredicateKind::Ambiguous - | PredicateKind::ClosureKind(_, _, _) | PredicateKind::Coerce(_) | PredicateKind::ConstEquate(_, _) | PredicateKind::ObjectSafe(_) + | PredicateKind::NormalizesTo(_) | PredicateKind::Subtype(_) => error_or_panic!( self, span, diff --git a/charon/src/translate/translate_traits.rs b/charon/src/translate/translate_traits.rs index 2ab213386..7494c8599 100644 --- a/charon/src/translate/translate_traits.rs +++ b/charon/src/translate/translate_traits.rs @@ -209,7 +209,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let trait_pred = rustc_middle::ty::TraitPredicate { trait_ref, // Not really necessary - polarity: rustc_middle::ty::ImplPolarity::Positive, + polarity: rustc_middle::ty::PredicatePolarity::Positive, }; let trait_pred = trait_pred.sinto(&self.hax_state); @@ -393,7 +393,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } if item_meta.opacity.is_opaque() { let ctx = bt_ctx.into_fmt(); - bt_ctx.t_ctx.errors.session.span_warn( + bt_ctx.t_ctx.errors.dcx.span_warn( item_meta.span, format!( "Trait declarations cannot be \"opaque\"; the trait `{}` will be translated as normal.", @@ -598,7 +598,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> { } if item_meta.opacity.is_opaque() { let ctx = bt_ctx.into_fmt(); - bt_ctx.t_ctx.errors.session.span_warn( + bt_ctx.t_ctx.errors.dcx.span_warn( item_meta.span, format!( "Trait implementations cannot be \"opaque\"; the impl `{}` will be translated as normal.", diff --git a/charon/src/translate/translate_types.rs b/charon/src/translate/translate_types.rs index 10a3951b6..35bcf08fa 100644 --- a/charon/src/translate/translate_types.rs +++ b/charon/src/translate/translate_types.rs @@ -278,10 +278,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { }; Ok(Ty::Ref(region, Box::new(ty), kind)) } - hax::Ty::RawPtr(ty_and_mut) => { - trace!("RawPtr: {:?}", ty_and_mut); - let ty = self.translate_ty(span, erase_regions, &ty_and_mut.ty)?; - let kind = if ty_and_mut.mutbl { + hax::Ty::RawPtr(ty, mutbl) => { + trace!("RawPtr: {:?}", (ty, mutbl)); + let ty = self.translate_ty(span, erase_regions, ty)?; + let kind = if *mutbl { RefKind::Mut } else { RefKind::Shared @@ -342,7 +342,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { error_or_panic!(self, span, "Dynamic types are not supported yet") } - hax::Ty::Coroutine(_, _, _) => { + hax::Ty::Coroutine(..) => { trace!("Coroutine"); error_or_panic!(self, span, "Coroutine types are not supported yet") } @@ -436,16 +436,17 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { let mut regions: Vec = vec![]; let mut params = vec![]; let mut cgs = vec![]; + use hax::GenericArg::*; for param in substs.iter() { match param { - hax::GenericArg::Type(param_ty) => { + Type(param_ty) => { let param_ty = self.translate_ty(span, erase_regions, param_ty)?; params.push(param_ty); } - hax::GenericArg::Lifetime(region) => { + Lifetime(region) => { regions.push(self.translate_region(span, erase_regions, region)?); } - hax::GenericArg::Const(c) => { + Const(c) => { cgs.push(self.translate_constant_expr_to_const_generic(span, c)?); } } @@ -522,9 +523,8 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> { } // Separate path for type aliases because they're not an `AdtDef`. - if let Some(local_def_id) = rust_id.as_local() { - let hir_id = tcx.hir().local_def_id_to_hir_id(local_def_id); - let rustc_hir::Node::Item(item) = tcx.hir().get(hir_id) else { + if let Some(node) = tcx.hir().get_if_local(rust_id) { + let rustc_hir::Node::Item(item) = node else { error_or_panic!(self, def_span, "Type is not an item?") }; if let rustc_hir::ItemKind::TyAlias(ty, _generics) = &item.kind { diff --git a/charon/tests/cargo/build-script/src/main.rs b/charon/tests/cargo/build-script/src/main.rs index 07266487d..b3328096a 100644 --- a/charon/tests/cargo/build-script/src/main.rs +++ b/charon/tests/cargo/build-script/src/main.rs @@ -1,3 +1,4 @@ +#![allow(unexpected_cfgs)] #[cfg(abc)] const FOO: u8 = 42; diff --git a/charon/tests/cargo/toml.out b/charon/tests/cargo/toml.out index 251fa78eb..f701f57ab 100644 --- a/charon/tests/cargo/toml.out +++ b/charon/tests/cargo/toml.out @@ -9,17 +9,15 @@ fn core::option::{core::option::Option}::is_some<'_0, T>(@1: &'_0 (core::opti { let @0: bool; // return let self@1: &'_ (core::option::Option); // arg #1 - let @2: isize; // anonymous local match *(self@1) { - 0 => { - @2 := const (0 : isize) - }, 1 => { - @2 := const (1 : isize) + @0 := const (true) + }, + 0 => { + @0 := const (false) } } - @0 := copy (@2) == const (1 : isize) return } diff --git a/charon/tests/cargo/toml/src/main.rs b/charon/tests/cargo/toml/src/main.rs index af8f4c9f4..7dcdd05b7 100644 --- a/charon/tests/cargo/toml/src/main.rs +++ b/charon/tests/cargo/toml/src/main.rs @@ -1,3 +1,4 @@ +#![allow(unexpected_cfgs)] // The `cfg` is here to test that we correctly passed rustc flags from the `Charon.toml`. The call // to `is_some` is here to exercice the `extract_opaque_bodies` option. #[cfg(abc)] diff --git a/charon/tests/crate_data.rs b/charon/tests/crate_data.rs index ed297bcf9..884e0a4a6 100644 --- a/charon/tests/crate_data.rs +++ b/charon/tests/crate_data.rs @@ -77,6 +77,7 @@ fn trait_name(crate_data: &CrateData, trait_id: TraitDeclId) -> &str { } #[derive(EnumAsGetters)] +#[expect(dead_code)] enum ItemKind<'c> { Fun(&'c FunDecl), Global(&'c GlobalDecl), diff --git a/charon/tests/ui/arrays.out b/charon/tests/ui/arrays.out index 94d422aa1..10ab6c6f2 100644 --- a/charon/tests/ui/arrays.out +++ b/charon/tests/ui/arrays.out @@ -1144,15 +1144,15 @@ fn test_crate::sum<'_0>(@1: &'_0 (Slice)) -> u32 drop @10 drop @11 i@3 := copy (i@3) + const (1 : usize) - @13 := () - @5 := move (@13) + @14 := () + @5 := move (@14) drop @6 continue 0 } drop @8 drop @7 - @14 := () - @4 := move (@14) + @13 := () + @4 := move (@13) drop @12 drop @6 drop @4 @@ -1532,15 +1532,15 @@ fn test_crate::zero_slice<'_0>(@1: &'_0 mut (Slice)) *(@14) := const (0 : u8) drop @9 i@2 := copy (i@2) + const (1 : usize) - @11 := () - @5 := move (@11) + @12 := () + @5 := move (@12) drop @6 continue 0 } drop @8 drop @7 - @12 := () - @0 := move (@12) + @11 := () + @0 := move (@11) drop @10 drop @6 drop len@3 @@ -1646,15 +1646,15 @@ fn test_crate::sum_mut_slice<'_0>(@1: &'_0 mut (Slice)) -> u32 drop @10 drop @11 i@2 := copy (i@2) + const (1 : usize) - @13 := () - @5 := move (@13) + @14 := () + @5 := move (@14) drop @6 continue 0 } drop @8 drop @7 - @14 := () - @4 := move (@14) + @13 := () + @4 := move (@13) drop @12 drop @6 drop @4 diff --git a/charon/tests/ui/external.out b/charon/tests/ui/external.out index 1c8743a5c..a23d750f9 100644 --- a/charon/tests/ui/external.out +++ b/charon/tests/ui/external.out @@ -19,28 +19,90 @@ fn test_crate::swap<'a, T>(@1: &'a mut (T), @2: &'a mut (T)) return } -opaque type core::num::nonzero::NonZeroU32 +trait core::clone::Clone +{ + fn clone : core::clone::Clone::clone + fn clone_from +} + +trait core::marker::Copy +{ + parent_clause_0 : [@TraitClause0]: core::clone::Clone +} + +trait core::num::nonzero::private::Sealed + +trait core::num::nonzero::ZeroablePrimitive +{ + parent_clause_0 : [@TraitClause0]: core::marker::Copy + parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + type NonZeroInner + where + [@TraitClause0]: core::marker::Copy, + [@TraitClause1]: core::clone::Clone, +} + +opaque type core::num::nonzero::NonZero + where + [@TraitClause0]: core::num::nonzero::ZeroablePrimitive, + +fn core::clone::impls::{impl core::clone::Clone for u32#8}::clone<'_0>(@1: &'_0 (u32)) -> u32 + +impl core::clone::impls::{impl core::clone::Clone for u32#8} : core::clone::Clone +{ + fn clone = core::clone::impls::{impl core::clone::Clone for u32#8}::clone +} + +impl core::marker::{impl core::marker::Copy for u32#41} : core::marker::Copy +{ + parent_clause0 = core::clone::impls::{impl core::clone::Clone for u32#8} +} + +impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for u32#19} : core::num::nonzero::private::Sealed + +opaque type core::num::nonzero::private::NonZeroU32Inner + +fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner#11}::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroU32Inner)) -> core::num::nonzero::private::NonZeroU32Inner + +impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner#11} : core::clone::Clone +{ + fn clone = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner#11}::clone +} + +impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroU32Inner#12} : core::marker::Copy +{ + parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner#11} +} + +impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for u32#20} : core::num::nonzero::ZeroablePrimitive +{ + parent_clause0 = core::marker::{impl core::marker::Copy for u32#41} + parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for u32#19} + type NonZeroInner = core::num::nonzero::private::NonZeroU32Inner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroU32Inner#12}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroU32Inner#11}] +} enum core::option::Option = | None() | Some(T) -fn core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new(@1: u32) -> core::option::Option +fn core::num::nonzero::{core::num::nonzero::NonZero#14}::new(@1: T) -> core::option::Option> +where + [@TraitClause0]: core::num::nonzero::ZeroablePrimitive, fn core::option::{core::option::Option}::unwrap(@1: core::option::Option) -> T -fn test_crate::test_new_non_zero_u32(@1: u32) -> core::num::nonzero::NonZeroU32 +fn test_crate::test_new_non_zero_u32(@1: u32) -> core::num::nonzero::NonZero { - let @0: core::num::nonzero::NonZeroU32; // return + let @0: core::num::nonzero::NonZero; // return let x@1: u32; // arg #1 - let @2: core::option::Option; // anonymous local + let @2: core::option::Option>; // anonymous local let @3: u32; // anonymous local @3 := copy (x@1) - @2 := core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new(move (@3)) + @2 := core::num::nonzero::{core::num::nonzero::NonZero#14}::new[core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for u32#20}](move (@3)) drop @3 - @0 := core::option::{core::option::Option}::unwrap(move (@2)) + @0 := core::option::{core::option::Option}::unwrap>(move (@2)) drop @2 return } @@ -77,33 +139,10 @@ fn test_crate::test_vec_push() opaque type core::cell::Cell -trait core::clone::Clone -{ - fn clone : core::clone::Clone::clone - fn clone_from -} - -trait core::marker::Copy -{ - parent_clause_0 : [@TraitClause0]: core::clone::Clone -} - fn core::cell::{core::cell::Cell#10}::get<'_0, T>(@1: &'_0 (core::cell::Cell)) -> T where [@TraitClause0]: core::marker::Copy, -fn core::clone::impls::{impl core::clone::Clone for u32#8}::clone<'_0>(@1: &'_0 (u32)) -> u32 - -impl core::clone::impls::{impl core::clone::Clone for u32#8} : core::clone::Clone -{ - fn clone = core::clone::impls::{impl core::clone::Clone for u32#8}::clone -} - -impl core::marker::{impl core::marker::Copy for u32#61} : core::marker::Copy -{ - parent_clause0 = core::clone::impls::{impl core::clone::Clone for u32#8} -} - fn test_crate::use_get<'_0>(@1: &'_0 (core::cell::Cell)) -> u32 { let @0: u32; // return @@ -111,7 +150,7 @@ fn test_crate::use_get<'_0>(@1: &'_0 (core::cell::Cell)) -> u32 let @2: &'_ (core::cell::Cell); // anonymous local @2 := &*(rc@1) - @0 := core::cell::{core::cell::Cell#10}::get[core::marker::{impl core::marker::Copy for u32#61}](move (@2)) + @0 := core::cell::{core::cell::Cell#10}::get[core::marker::{impl core::marker::Copy for u32#41}](move (@2)) drop @2 return } diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index e3d3bee61..855400fec 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -63,24 +63,16 @@ fn core::bool::{bool}::then_some(@1: bool, @2: T) -> core::option::Option let self@1: bool; // arg #1 let t@2: T; // arg #2 let @3: T; // anonymous local - let @4: bool; // anonymous local - @4 := const (true) if copy (self@1) { - @4 := const (false) @3 := move (t@2) @0 := core::option::Option::Some { 0: move (@3) } drop @3 } else { @0 := core::option::Option::None { } - } - if copy (@4) { drop t@2 } - else { - nop - } return } @@ -104,7 +96,7 @@ trait core::convert::From fn from : core::convert::From::from } -fn core::convert::num::{impl core::convert::From for i64#59}::from(@1: i32) -> i64 +fn core::convert::num::{impl core::convert::From for i64#83}::from(@1: i32) -> i64 { let @0: i64; // return let small@1: i32; // arg #1 @@ -113,9 +105,9 @@ fn core::convert::num::{impl core::convert::From for i64#59}::from(@1: i32) return } -impl core::convert::num::{impl core::convert::From for i64#59} : core::convert::From +impl core::convert::num::{impl core::convert::From for i64#83} : core::convert::From { - fn from = core::convert::num::{impl core::convert::From for i64#59}::from + fn from = core::convert::num::{impl core::convert::From for i64#83}::from } fn core::convert::From::from(@1: T) -> Self @@ -127,7 +119,7 @@ fn test_crate::convert(@1: i32) -> i64 let @2: i32; // anonymous local @2 := copy (x@1) - @0 := core::convert::num::{impl core::convert::From for i64#59}::from(move (@2)) + @0 := core::convert::num::{impl core::convert::From for i64#83}::from(move (@2)) drop @2 return } @@ -145,10 +137,15 @@ struct core::ptr::unique::Unique = _marker: core::marker::PhantomData } +struct alloc::raw_vec::Cap = +{ + usize +} + struct alloc::raw_vec::RawVec = { ptr: core::ptr::unique::Unique, - cap: usize, + cap: alloc::raw_vec::Cap, alloc: A } diff --git a/charon/tests/ui/issue-120-bare-discriminant-read.out b/charon/tests/ui/issue-120-bare-discriminant-read.out index 6a052a521..e8511c53b 100644 --- a/charon/tests/ui/issue-120-bare-discriminant-read.out +++ b/charon/tests/ui/issue-120-bare-discriminant-read.out @@ -9,21 +9,17 @@ fn test_crate::call_is_some(@1: core::option::Option) -> bool { let @0: bool; // return let opt@1: core::option::Option; // arg #1 - let self@2: &'_ (core::option::Option); // local - let @3: isize; // anonymous local + let @2: isize; // anonymous local - self@2 := &opt@1 match opt@1 { - 0 => { - @3 := const (0 : isize) - }, 1 => { - @3 := const (1 : isize) + @0 := const (true) + }, + 0 => { + @0 := const (false) } } - @0 := copy (@3) == const (1 : isize) - drop @3 - drop self@2 + drop @2 drop opt@1 return } diff --git a/charon/tests/ui/issue-4-slice-try-into-array.out b/charon/tests/ui/issue-4-slice-try-into-array.out index 4a91ebb99..247a805d8 100644 --- a/charon/tests/ui/issue-4-slice-try-into-array.out +++ b/charon/tests/ui/issue-4-slice-try-into-array.out @@ -63,7 +63,7 @@ impl core::clone::impls::{impl core::clone::Clone for u8#6} : core::clone::Clone fn clone = core::clone::impls::{impl core::clone::Clone for u8#6}::clone } -impl core::marker::{impl core::marker::Copy for u8#59} : core::marker::Copy +impl core::marker::{impl core::marker::Copy for u8#39} : core::marker::Copy { parent_clause0 = core::clone::impls::{impl core::clone::Clone for u8#6} } @@ -102,7 +102,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice)) let @5: (); // anonymous local @4 := &*(s@1) - @3 := core::convert::{impl core::convert::TryInto for T#6}<&'_ (Slice), Array>[core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array#7}<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8#59}]]::try_into(move (@4)) + @3 := core::convert::{impl core::convert::TryInto for T#6}<&'_ (Slice), Array>[core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array#7}<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8#39}]]::try_into(move (@4)) drop @4 _array@2 := core::result::{core::result::Result}::unwrap, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError#26}](move (@3)) drop @3 diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index 4a91ebb99..247a805d8 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -63,7 +63,7 @@ impl core::clone::impls::{impl core::clone::Clone for u8#6} : core::clone::Clone fn clone = core::clone::impls::{impl core::clone::Clone for u8#6}::clone } -impl core::marker::{impl core::marker::Copy for u8#59} : core::marker::Copy +impl core::marker::{impl core::marker::Copy for u8#39} : core::marker::Copy { parent_clause0 = core::clone::impls::{impl core::clone::Clone for u8#6} } @@ -102,7 +102,7 @@ fn test_crate::trait_error<'_0>(@1: &'_0 (Slice)) let @5: (); // anonymous local @4 := &*(s@1) - @3 := core::convert::{impl core::convert::TryInto for T#6}<&'_ (Slice), Array>[core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array#7}<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8#59}]]::try_into(move (@4)) + @3 := core::convert::{impl core::convert::TryInto for T#6}<&'_ (Slice), Array>[core::array::{impl core::convert::TryFrom<&'_0 (Slice)> for Array#7}<'_, u8, 4 : usize>[core::marker::{impl core::marker::Copy for u8#39}]]::try_into(move (@4)) drop @4 _array@2 := core::result::{core::result::Result}::unwrap, core::array::TryFromSliceError>[core::array::{impl core::fmt::Debug for core::array::TryFromSliceError#26}](move (@3)) drop @3 diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 6801961fe..5a11b1f09 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -154,18 +154,18 @@ where fn into_iter : core::iter::traits::collect::IntoIterator::into_iter } -fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}::into_iter(@1: I) -> I +fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter(@1: I) -> I where // Inherited clauses: [@TraitClause0]: core::iter::traits::iterator::Iterator, -impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I} : core::iter::traits::collect::IntoIterator +impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1} : core::iter::traits::collect::IntoIterator where [@TraitClause0]: core::iter::traits::iterator::Iterator, { type Item = @TraitClause0::Item with [] type IntoIter = I with [@TraitClause0] - fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}::into_iter + fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter } trait core::clone::Clone @@ -274,9 +274,63 @@ enum core::result::Result = | Err(E) -opaque type core::num::nonzero::NonZeroUsize +trait core::marker::Copy +{ + parent_clause_0 : [@TraitClause0]: core::clone::Clone +} + +trait core::num::nonzero::private::Sealed + +trait core::num::nonzero::ZeroablePrimitive +{ + parent_clause_0 : [@TraitClause0]: core::marker::Copy + parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + type NonZeroInner + where + [@TraitClause0]: core::marker::Copy, + [@TraitClause1]: core::clone::Clone, +} + +opaque type core::num::nonzero::NonZero + where + [@TraitClause0]: core::num::nonzero::ZeroablePrimitive, + +fn core::clone::impls::{impl core::clone::Clone for usize#5}::clone<'_0>(@1: &'_0 (usize)) -> usize -fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZeroUsize> +impl core::clone::impls::{impl core::clone::Clone for usize#5} : core::clone::Clone +{ + fn clone = core::clone::impls::{impl core::clone::Clone for usize#5}::clone +} + +impl core::marker::{impl core::marker::Copy for usize#38} : core::marker::Copy +{ + parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize#5} +} + +impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} : core::num::nonzero::private::Sealed + +opaque type core::num::nonzero::private::NonZeroUsizeInner + +fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner + +impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} : core::clone::Clone +{ + fn clone = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}::clone +} + +impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27} : core::marker::Copy +{ + parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} +} + +impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize#26} : core::num::nonzero::ZeroablePrimitive +{ + parent_clause0 = core::marker::{impl core::marker::Copy for usize#38} + parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} + type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}] +} + +fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero> where // Inherited clauses: [@TraitClause0]: core::iter::range::Step, @@ -328,24 +382,24 @@ impl core::cmp::impls::{impl core::cmp::PartialEq for u8#22} : core::cmp::Pa fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u8#22}::ne } -fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::partial_cmp<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option +fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::partial_cmp<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option -fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::lt<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::lt<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::le<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::le<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::ge<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::ge<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::gt<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::gt<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialOrd for u8#56} : core::cmp::PartialOrd +impl core::cmp::impls::{impl core::cmp::PartialOrd for u8#60} : core::cmp::PartialOrd { parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u8#22} - fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::partial_cmp - fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::lt - fn le = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::le - fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::ge - fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56}::gt + fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::partial_cmp + fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::lt + fn le = core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::le + fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::ge + fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for u8#60}::gt } fn core::iter::range::{impl core::iter::range::Step for u8#35}::steps_between<'_0, '_1>(@1: &'_0 (u8), @2: &'_1 (u8)) -> core::option::Option @@ -354,25 +408,25 @@ fn core::iter::range::{impl core::iter::range::Step for u8#35}::forward_checked( fn core::iter::range::{impl core::iter::range::Step for u8#35}::backward_checked(@1: u8, @2: usize) -> core::option::Option -unsafe fn core::iter::range::{impl core::iter::range::Step for u8#35}::forward_unchecked(@1: u8, @2: usize) -> u8 - -unsafe fn core::iter::range::{impl core::iter::range::Step for u8#35}::backward_unchecked(@1: u8, @2: usize) -> u8 - fn core::iter::range::{impl core::iter::range::Step for u8#35}::forward(@1: u8, @2: usize) -> u8 fn core::iter::range::{impl core::iter::range::Step for u8#35}::backward(@1: u8, @2: usize) -> u8 +unsafe fn core::iter::range::{impl core::iter::range::Step for u8#35}::forward_unchecked(@1: u8, @2: usize) -> u8 + +unsafe fn core::iter::range::{impl core::iter::range::Step for u8#35}::backward_unchecked(@1: u8, @2: usize) -> u8 + impl core::iter::range::{impl core::iter::range::Step for u8#35} : core::iter::range::Step { parent_clause0 = core::clone::impls::{impl core::clone::Clone for u8#6} - parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for u8#56} + parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for u8#60} fn steps_between = core::iter::range::{impl core::iter::range::Step for u8#35}::steps_between fn forward_checked = core::iter::range::{impl core::iter::range::Step for u8#35}::forward_checked fn backward_checked = core::iter::range::{impl core::iter::range::Step for u8#35}::backward_checked - fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for u8#35}::forward_unchecked - fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for u8#35}::backward_unchecked fn forward = core::iter::range::{impl core::iter::range::Step for u8#35}::forward fn backward = core::iter::range::{impl core::iter::range::Step for u8#35}::backward + fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for u8#35}::forward_unchecked + fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for u8#35}::backward_unchecked } fn core::iter::traits::collect::IntoIterator::into_iter(@1: Self) -> Self::IntoIter @@ -401,7 +455,7 @@ fn test_crate::cbd(@1: Array) let @17: &'_ mut (u8); // anonymous local @3 := core::ops::range::Range { start: const (0 : u8), end: const (3 : u8) } - @2 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for u8#35}]]::into_iter(move (@3)) + @2 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for u8#35}]]::into_iter(move (@3)) drop @3 @fake_read(@2) iter@4 := move (@2) diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out index cca7bd8d9..dd0876c50 100644 --- a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out +++ b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out @@ -4,7 +4,7 @@ error: Unsupported statement kind: intrinsic 16 | let _ = x as isize; | ^^^^^^^^^^ -error: aborting due to previous error +error: aborting due to 1 previous error -[ ERROR charon_driver:231] The extraction encountered 1 errors +[ ERROR charon_driver:230] The extraction encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/loops.out b/charon/tests/ui/loops.out index a15833fdc..5d142e95c 100644 --- a/charon/tests/ui/loops.out +++ b/charon/tests/ui/loops.out @@ -91,8 +91,8 @@ fn test_crate::test_loop2(@1: u32) -> u32 @10 := move (@11) == const (17 : u32) if move (@10) { drop @11 - @14 := () - @4 := move (@14) + @15 := () + @4 := move (@15) drop @10 drop @9 break 0 @@ -116,8 +116,8 @@ fn test_crate::test_loop2(@1: u32) -> u32 else { drop @8 drop @7 - @15 := () - @4 := move (@15) + @14 := () + @4 := move (@14) drop @13 break 0 } @@ -201,8 +201,8 @@ fn test_crate::test_loop3(@1: u32) -> u32 } else { drop @16 - @25 := () - @14 := move (@25) + @26 := () + @14 := move (@26) drop @15 drop @14 @19 := copy (i@2) @@ -232,8 +232,8 @@ fn test_crate::test_loop3(@1: u32) -> u32 s@4 := copy (s@4) + move (@21) drop @21 i@2 := copy (i@2) + const (1 : u32) - @26 := () - @6 := move (@26) + @25 := () + @6 := move (@25) drop @7 continue 0 } @@ -317,8 +317,8 @@ fn test_crate::test_loop4(@1: u32) -> u32 } else { drop @16 - @25 := () - @14 := move (@25) + @26 := () + @14 := move (@26) drop @15 drop @14 @19 := copy (i@2) @@ -348,8 +348,8 @@ fn test_crate::test_loop4(@1: u32) -> u32 s@4 := copy (s@4) + move (@21) drop @21 i@2 := copy (i@2) + const (1 : u32) - @26 := () - @6 := move (@26) + @25 := () + @6 := move (@25) drop @7 continue 0 } @@ -501,8 +501,8 @@ fn test_crate::test_loop6(@1: u32) -> u32 @10 := move (@11) > const (3 : u32) if move (@10) { drop @11 - @14 := () - @4 := move (@14) + @15 := () + @4 := move (@15) drop @10 drop @9 break 0 @@ -526,8 +526,8 @@ fn test_crate::test_loop6(@1: u32) -> u32 else { drop @8 drop @7 - @15 := () - @4 := move (@15) + @14 := () + @4 := move (@14) drop @13 break 0 } @@ -587,8 +587,8 @@ fn test_crate::test_loop7(@1: u32) -> u32 @13 := move (@14) > const (3 : u32) if move (@13) { drop @14 - @18 := () - @4 := move (@18) + @19 := () + @4 := move (@19) drop @13 drop @12 break 0 @@ -612,8 +612,8 @@ fn test_crate::test_loop7(@1: u32) -> u32 else { drop @11 drop @10 - @19 := () - @4 := move (@19) + @18 := () + @4 := move (@18) drop @16 break 0 } @@ -883,18 +883,18 @@ where fn into_iter : core::iter::traits::collect::IntoIterator::into_iter } -fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}::into_iter(@1: I) -> I +fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter(@1: I) -> I where // Inherited clauses: [@TraitClause0]: core::iter::traits::iterator::Iterator, -impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I} : core::iter::traits::collect::IntoIterator +impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1} : core::iter::traits::collect::IntoIterator where [@TraitClause0]: core::iter::traits::iterator::Iterator, { type Item = @TraitClause0::Item with [] type IntoIter = I with [@TraitClause0] - fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}::into_iter + fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter } trait core::clone::Clone @@ -1003,9 +1003,63 @@ enum core::result::Result = | Err(E) -opaque type core::num::nonzero::NonZeroUsize +trait core::marker::Copy +{ + parent_clause_0 : [@TraitClause0]: core::clone::Clone +} + +trait core::num::nonzero::private::Sealed + +trait core::num::nonzero::ZeroablePrimitive +{ + parent_clause_0 : [@TraitClause0]: core::marker::Copy + parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + type NonZeroInner + where + [@TraitClause0]: core::marker::Copy, + [@TraitClause1]: core::clone::Clone, +} + +opaque type core::num::nonzero::NonZero + where + [@TraitClause0]: core::num::nonzero::ZeroablePrimitive, + +fn core::clone::impls::{impl core::clone::Clone for usize#5}::clone<'_0>(@1: &'_0 (usize)) -> usize + +impl core::clone::impls::{impl core::clone::Clone for usize#5} : core::clone::Clone +{ + fn clone = core::clone::impls::{impl core::clone::Clone for usize#5}::clone +} + +impl core::marker::{impl core::marker::Copy for usize#38} : core::marker::Copy +{ + parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize#5} +} + +impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} : core::num::nonzero::private::Sealed + +opaque type core::num::nonzero::private::NonZeroUsizeInner + +fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner + +impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} : core::clone::Clone +{ + fn clone = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}::clone +} + +impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27} : core::marker::Copy +{ + parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} +} + +impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize#26} : core::num::nonzero::ZeroablePrimitive +{ + parent_clause0 = core::marker::{impl core::marker::Copy for usize#38} + parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} + type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}] +} -fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZeroUsize> +fn core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}::advance_by<'_0, A>(@1: &'_0 mut (core::ops::range::Range), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero> where // Inherited clauses: [@TraitClause0]: core::iter::range::Step, @@ -1057,24 +1111,24 @@ impl core::cmp::impls::{impl core::cmp::PartialEq for i32#30} : core::cmp:: fn ne = core::cmp::impls::{impl core::cmp::PartialEq for i32#30}::ne } -fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::partial_cmp<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option +fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::partial_cmp<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option -fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::lt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::lt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::le<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::le<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::ge<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::ge<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::gt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::gt<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialOrd for i32#72} : core::cmp::PartialOrd +impl core::cmp::impls::{impl core::cmp::PartialOrd for i32#76} : core::cmp::PartialOrd { parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for i32#30} - fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::partial_cmp - fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::lt - fn le = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::le - fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::ge - fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72}::gt + fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::partial_cmp + fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::lt + fn le = core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::le + fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::ge + fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for i32#76}::gt } fn core::iter::range::{impl core::iter::range::Step for i32#40}::steps_between<'_0, '_1>(@1: &'_0 (i32), @2: &'_1 (i32)) -> core::option::Option @@ -1083,38 +1137,31 @@ fn core::iter::range::{impl core::iter::range::Step for i32#40}::forward_checked fn core::iter::range::{impl core::iter::range::Step for i32#40}::backward_checked(@1: i32, @2: usize) -> core::option::Option -unsafe fn core::iter::range::{impl core::iter::range::Step for i32#40}::forward_unchecked(@1: i32, @2: usize) -> i32 - -unsafe fn core::iter::range::{impl core::iter::range::Step for i32#40}::backward_unchecked(@1: i32, @2: usize) -> i32 - fn core::iter::range::{impl core::iter::range::Step for i32#40}::forward(@1: i32, @2: usize) -> i32 fn core::iter::range::{impl core::iter::range::Step for i32#40}::backward(@1: i32, @2: usize) -> i32 +unsafe fn core::iter::range::{impl core::iter::range::Step for i32#40}::forward_unchecked(@1: i32, @2: usize) -> i32 + +unsafe fn core::iter::range::{impl core::iter::range::Step for i32#40}::backward_unchecked(@1: i32, @2: usize) -> i32 + impl core::iter::range::{impl core::iter::range::Step for i32#40} : core::iter::range::Step { parent_clause0 = core::clone::impls::{impl core::clone::Clone for i32#14} - parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for i32#72} + parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for i32#76} fn steps_between = core::iter::range::{impl core::iter::range::Step for i32#40}::steps_between fn forward_checked = core::iter::range::{impl core::iter::range::Step for i32#40}::forward_checked fn backward_checked = core::iter::range::{impl core::iter::range::Step for i32#40}::backward_checked - fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for i32#40}::forward_unchecked - fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for i32#40}::backward_unchecked fn forward = core::iter::range::{impl core::iter::range::Step for i32#40}::forward fn backward = core::iter::range::{impl core::iter::range::Step for i32#40}::backward + fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for i32#40}::forward_unchecked + fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for i32#40}::backward_unchecked } fn core::iter::traits::collect::IntoIterator::into_iter(@1: Self) -> Self::IntoIter fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option -fn core::clone::impls::{impl core::clone::Clone for usize#5}::clone<'_0>(@1: &'_0 (usize)) -> usize - -impl core::clone::impls::{impl core::clone::Clone for usize#5} : core::clone::Clone -{ - fn clone = core::clone::impls::{impl core::clone::Clone for usize#5}::clone -} - fn core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::eq<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool fn core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::ne<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool @@ -1125,24 +1172,24 @@ impl core::cmp::impls::{impl core::cmp::PartialEq for usize#21} : core::c fn ne = core::cmp::impls::{impl core::cmp::PartialEq for usize#21}::ne } -fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::partial_cmp<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option +fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::partial_cmp<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option -fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::lt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::lt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::le<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::le<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::ge<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::ge<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::gt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::gt<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialOrd for usize#54} : core::cmp::PartialOrd +impl core::cmp::impls::{impl core::cmp::PartialOrd for usize#58} : core::cmp::PartialOrd { parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for usize#21} - fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::partial_cmp - fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::lt - fn le = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::le - fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::ge - fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54}::gt + fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::partial_cmp + fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::lt + fn le = core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::le + fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::ge + fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for usize#58}::gt } fn core::iter::range::{impl core::iter::range::Step for usize#43}::steps_between<'_0, '_1>(@1: &'_0 (usize), @2: &'_1 (usize)) -> core::option::Option @@ -1151,25 +1198,25 @@ fn core::iter::range::{impl core::iter::range::Step for usize#43}::forward_check fn core::iter::range::{impl core::iter::range::Step for usize#43}::backward_checked(@1: usize, @2: usize) -> core::option::Option -unsafe fn core::iter::range::{impl core::iter::range::Step for usize#43}::forward_unchecked(@1: usize, @2: usize) -> usize - -unsafe fn core::iter::range::{impl core::iter::range::Step for usize#43}::backward_unchecked(@1: usize, @2: usize) -> usize - fn core::iter::range::{impl core::iter::range::Step for usize#43}::forward(@1: usize, @2: usize) -> usize fn core::iter::range::{impl core::iter::range::Step for usize#43}::backward(@1: usize, @2: usize) -> usize +unsafe fn core::iter::range::{impl core::iter::range::Step for usize#43}::forward_unchecked(@1: usize, @2: usize) -> usize + +unsafe fn core::iter::range::{impl core::iter::range::Step for usize#43}::backward_unchecked(@1: usize, @2: usize) -> usize + impl core::iter::range::{impl core::iter::range::Step for usize#43} : core::iter::range::Step { parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize#5} - parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for usize#54} + parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for usize#58} fn steps_between = core::iter::range::{impl core::iter::range::Step for usize#43}::steps_between fn forward_checked = core::iter::range::{impl core::iter::range::Step for usize#43}::forward_checked fn backward_checked = core::iter::range::{impl core::iter::range::Step for usize#43}::backward_checked - fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for usize#43}::forward_unchecked - fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for usize#43}::backward_unchecked fn forward = core::iter::range::{impl core::iter::range::Step for usize#43}::forward fn backward = core::iter::range::{impl core::iter::range::Step for usize#43}::backward + fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for usize#43}::forward_unchecked + fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for usize#43}::backward_unchecked } fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize @@ -1216,7 +1263,7 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize s@3 := const (0 : usize) @fake_read(s@3) @6 := core::ops::range::Range { start: const (0 : i32), end: const (128 : i32) } - @5 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for i32#40}]]::into_iter(move (@6)) + @5 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for i32#40}]]::into_iter(move (@6)) drop @6 @fake_read(@5) iter@7 := move (@5) @@ -1237,14 +1284,14 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize drop @12 drop @10 drop @9 - @32 := () - @8 := move (@32) + @31 := () + @8 := move (@31) continue 0 } } } - @31 := () - @4 := move (@31) + @32 := () + @4 := move (@32) drop @12 drop @10 drop @9 @@ -1254,7 +1301,7 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize @16 := copy (step_out@1) @15 := core::ops::range::Range { start: const (0 : usize), end: move (@16) } drop @16 - @14 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for usize#43}]]::into_iter(move (@15)) + @14 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for usize#43}]]::into_iter(move (@15)) drop @15 @fake_read(@14) iter@17 := move (@14) @@ -1272,7 +1319,7 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize @24 := copy (step_in@2) @23 := core::ops::range::Range { start: const (0 : usize), end: move (@24) } drop @24 - @22 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for usize#43}]]::into_iter(move (@23)) + @22 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for usize#43}]]::into_iter(move (@23)) drop @23 @fake_read(@22) iter@25 := move (@22) @@ -1293,14 +1340,14 @@ fn test_crate::nested_loops_enum(@1: usize, @2: usize) -> usize drop @29 drop @27 drop @26 - @36 := () - @8 := move (@36) + @35 := () + @8 := move (@35) continue 0 } } } - @35 := () - @18 := move (@35) + @36 := () + @18 := move (@36) drop @29 drop @27 drop @26 @@ -1345,24 +1392,24 @@ impl core::cmp::impls::{impl core::cmp::PartialEq for u32#24} : core::cmp:: fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne } -fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::partial_cmp<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option +fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::partial_cmp<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option -fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::lt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::lt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::le<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::le<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::ge<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::ge<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::gt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool +fn core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::gt<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> bool -impl core::cmp::impls::{impl core::cmp::PartialOrd for u32#60} : core::cmp::PartialOrd +impl core::cmp::impls::{impl core::cmp::PartialOrd for u32#64} : core::cmp::PartialOrd { parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32#24} - fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::partial_cmp - fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::lt - fn le = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::le - fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::ge - fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60}::gt + fn partial_cmp = core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::partial_cmp + fn lt = core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::lt + fn le = core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::le + fn ge = core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::ge + fn gt = core::cmp::impls::{impl core::cmp::PartialOrd for u32#64}::gt } fn core::iter::range::{impl core::iter::range::Step for u32#39}::steps_between<'_0, '_1>(@1: &'_0 (u32), @2: &'_1 (u32)) -> core::option::Option @@ -1371,25 +1418,25 @@ fn core::iter::range::{impl core::iter::range::Step for u32#39}::forward_checked fn core::iter::range::{impl core::iter::range::Step for u32#39}::backward_checked(@1: u32, @2: usize) -> core::option::Option -unsafe fn core::iter::range::{impl core::iter::range::Step for u32#39}::forward_unchecked(@1: u32, @2: usize) -> u32 - -unsafe fn core::iter::range::{impl core::iter::range::Step for u32#39}::backward_unchecked(@1: u32, @2: usize) -> u32 - fn core::iter::range::{impl core::iter::range::Step for u32#39}::forward(@1: u32, @2: usize) -> u32 fn core::iter::range::{impl core::iter::range::Step for u32#39}::backward(@1: u32, @2: usize) -> u32 +unsafe fn core::iter::range::{impl core::iter::range::Step for u32#39}::forward_unchecked(@1: u32, @2: usize) -> u32 + +unsafe fn core::iter::range::{impl core::iter::range::Step for u32#39}::backward_unchecked(@1: u32, @2: usize) -> u32 + impl core::iter::range::{impl core::iter::range::Step for u32#39} : core::iter::range::Step { parent_clause0 = core::clone::impls::{impl core::clone::Clone for u32#8} - parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for u32#60} + parent_clause1 = core::cmp::impls::{impl core::cmp::PartialOrd for u32#64} fn steps_between = core::iter::range::{impl core::iter::range::Step for u32#39}::steps_between fn forward_checked = core::iter::range::{impl core::iter::range::Step for u32#39}::forward_checked fn backward_checked = core::iter::range::{impl core::iter::range::Step for u32#39}::backward_checked - fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for u32#39}::forward_unchecked - fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for u32#39}::backward_unchecked fn forward = core::iter::range::{impl core::iter::range::Step for u32#39}::forward fn backward = core::iter::range::{impl core::iter::range::Step for u32#39}::backward + fn forward_unchecked = core::iter::range::{impl core::iter::range::Step for u32#39}::forward_unchecked + fn backward_unchecked = core::iter::range::{impl core::iter::range::Step for u32#39}::backward_unchecked } fn test_crate::loop_inside_if(@1: bool, @2: u32) -> u32 @@ -1422,7 +1469,7 @@ fn test_crate::loop_inside_if(@1: bool, @2: u32) -> u32 @8 := copy (n@2) @7 := core::ops::range::Range { start: const (0 : u32), end: move (@8) } drop @8 - @6 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for u32#39}]]::into_iter(move (@7)) + @6 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::iter::range::{impl core::iter::traits::iterator::Iterator for core::ops::range::Range#6}[core::iter::range::{impl core::iter::range::Step for u32#39}]]::into_iter(move (@7)) drop @7 @fake_read(@6) iter@9 := move (@6) @@ -1447,14 +1494,14 @@ fn test_crate::loop_inside_if(@1: bool, @2: u32) -> u32 drop @14 drop @12 drop @11 - @19 := () - @10 := move (@19) + @18 := () + @10 := move (@18) continue 0 } } } - @18 := () - @5 := move (@18) + @19 := () + @5 := move (@19) drop @14 drop @12 drop @11 @@ -1566,14 +1613,14 @@ fn test_crate::sum_array(@1: Array) -> u3 drop @8 drop @9 i@2 := copy (i@2) + const (1 : usize) - @11 := () - @5 := move (@11) + @12 := () + @5 := move (@12) drop @6 continue 0 } drop @7 - @12 := () - @4 := move (@12) + @11 := () + @4 := move (@11) drop @10 drop @6 drop @4 @@ -1615,30 +1662,30 @@ trait core::ops::index::IndexMut fn index_mut : core::ops::index::IndexMut::index_mut } -fn alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#12}::index<'_0, T, I, A>(@1: &'_0 (alloc::vec::Vec), @2: I) -> &'_0 (alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#12}[@TraitClause0]::Output) +fn alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#13}::index<'_0, T, I, A>(@1: &'_0 (alloc::vec::Vec), @2: I) -> &'_0 (alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#13}[@TraitClause0]::Output) where // Inherited clauses: [@TraitClause0]: core::slice::index::SliceIndex>, -impl alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#12} : core::ops::index::Index, I> +impl alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#13} : core::ops::index::Index, I> where [@TraitClause0]: core::slice::index::SliceIndex>, { type Output = @TraitClause0::Output with [] - fn index = alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#12}::index + fn index = alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#13}::index } -fn alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec#13}::index_mut<'_0, T, I, A>(@1: &'_0 mut (alloc::vec::Vec), @2: I) -> &'_0 mut (alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#12}[@TraitClause0]::Output) +fn alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec#14}::index_mut<'_0, T, I, A>(@1: &'_0 mut (alloc::vec::Vec), @2: I) -> &'_0 mut (alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#13}[@TraitClause0]::Output) where // Inherited clauses: [@TraitClause0]: core::slice::index::SliceIndex>, -impl alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec#13} : core::ops::index::IndexMut, I> +impl alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec#14} : core::ops::index::IndexMut, I> where [@TraitClause0]: core::slice::index::SliceIndex>, { - parent_clause0 = alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#12}[@TraitClause0] - fn index_mut = alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec#13}::index_mut + parent_clause0 = alloc::vec::{impl core::ops::index::Index for alloc::vec::Vec#13}[@TraitClause0] + fn index_mut = alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec#14}::index_mut } impl core::slice::index::private_slice_index::{impl core::slice::index::private_slice_index::Sealed for usize} : core::slice::index::private_slice_index::Sealed @@ -1704,21 +1751,21 @@ fn test_crate::clear<'_0>(@1: &'_0 mut (alloc::vec::Vec for alloc::vec::Vec#13}[core::slice::index::{impl core::slice::index::SliceIndex> for usize#2}]::index_mut(move (@9), move (@10)) + @8 := alloc::vec::{impl core::ops::index::IndexMut for alloc::vec::Vec#14}[core::slice::index::{impl core::slice::index::SliceIndex> for usize#2}]::index_mut(move (@9), move (@10)) drop @10 drop @9 *(@8) := const (0 : u32) drop @8 i@2 := copy (i@2) + const (1 : usize) - @12 := () - @3 := move (@12) + @13 := () + @3 := move (@13) drop @4 continue 0 } drop @6 drop @5 - @13 := () - @0 := move (@13) + @12 := () + @0 := move (@12) drop @11 drop @4 drop i@2 @@ -1864,8 +1911,6 @@ fn core::cmp::PartialOrd::partial_cmp<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: fn core::cmp::PartialEq::eq<'_0, '_1, Self, Rhs>(@1: &'_0 (Self), @2: &'_1 (Rhs)) -> bool -fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output) - fn core::slice::index::SliceIndex::get<'_0, Self, T>(@1: Self, @2: &'_0 (T)) -> core::option::Option<&'_0 (Self::Output)> fn core::slice::index::SliceIndex::get_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> core::option::Option<&'_0 mut (Self::Output)> @@ -1878,6 +1923,8 @@ fn core::slice::index::SliceIndex::index<'_0, Self, T>(@1: Self, @2: &'_0 (T)) - fn core::slice::index::SliceIndex::index_mut<'_0, Self, T>(@1: Self, @2: &'_0 mut (T)) -> &'_0 mut (Self::Output) +fn core::ops::index::Index::index<'_0, Self, Idx>(@1: &'_0 (Self), @2: Idx) -> &'_0 (Self::Output) + fn core::cmp::Ord::cmp<'_0, '_1, Self>(@1: &'_0 (Self), @2: &'_1 (Self)) -> core::cmp::Ordering diff --git a/charon/tests/ui/matches.out b/charon/tests/ui/matches.out index a3df35dac..87a2efa06 100644 --- a/charon/tests/ui/matches.out +++ b/charon/tests/ui/matches.out @@ -13,14 +13,19 @@ fn test_crate::test1(@1: test_crate::E1) -> bool @fake_read(x@1) match x@1 { - 0 => { - @0 := const (true) - }, - 1 => { + 0 | 1 => { @0 := const (true) }, - 2 => { - @0 := const (false) + _ => { + match x@1 { + 2 => { + @0 := const (false) + }, + _ => { + @fake_read(x@1) + undefined_behavior + } + } } } return @@ -60,8 +65,16 @@ fn test_crate::test2(@1: test_crate::E2) -> u32 @0 := copy (n@2) drop n@2 }, - 2 => { - @0 := const (0 : u32) + _ => { + match x@1 { + 2 => { + @0 := const (0 : u32) + }, + _ => { + @fake_read(x@1) + undefined_behavior + } + } } } return @@ -93,8 +106,16 @@ fn test_crate::test3(@1: test_crate::E2) -> u32 y@3 := copy (n@4) drop n@4 }, - 2 => { - y@3 := const (0 : u32) + _ => { + match x@1 { + 2 => { + y@3 := const (0 : u32) + }, + _ => { + @fake_read(x@1) + undefined_behavior + } + } } } @fake_read(y@3) diff --git a/charon/tests/ui/panics.out b/charon/tests/ui/panics.out index 394a82d8f..a23b8b60c 100644 --- a/charon/tests/ui/panics.out +++ b/charon/tests/ui/panics.out @@ -13,23 +13,20 @@ opaque type core::fmt::Arguments<'a> where 'a : 'a, -fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a>(@1: &'a (Slice<&'static (Str)>)) -> core::fmt::Arguments<'a> +fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : usize>)) -> core::fmt::Arguments<'a> fn test_crate::panic2() { let @0: (); // return let @1: core::fmt::Arguments<'_>; // anonymous local - let @2: &'_ (Slice<&'_ (Str)>); // anonymous local + let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: Array<&'_ (Str), 1 : usize>; // anonymous local - - @5 := [const ("O no!"); 1 : usize] - @4 := &@5 - @3 := &*(@4) - @2 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@3)) - drop @3 - @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_>(move (@2)) + let @4: Array<&'_ (Str), 1 : usize>; // anonymous local + + @4 := [const ("O no!"); 1 : usize] + @3 := &@4 + @2 := &*(@3) + @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_, 1 : usize>(move (@2)) drop @2 panic(core::panicking::panic_fmt) } @@ -38,33 +35,27 @@ opaque type core::fmt::rt::Argument<'a> fn core::fmt::rt::{core::fmt::rt::Argument<'a>#1}::none<'a>() -> Array, 0 : usize> -fn core::fmt::{core::fmt::Arguments<'a>#2}::new_v1<'a>(@1: &'a (Slice<&'static (Str)>), @2: &'a (Slice>)) -> core::fmt::Arguments<'a> +fn core::fmt::{core::fmt::Arguments<'a>#2}::new_v1<'a, const P : usize, const A : usize>(@1: &'a (Array<&'static (Str), const P : usize>), @2: &'a (Array, const A : usize>)) -> core::fmt::Arguments<'a> fn test_crate::panic3() { let @0: (); // return let @1: core::fmt::Arguments<'_>; // anonymous local - let @2: &'_ (Slice<&'_ (Str)>); // anonymous local + let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: Array<&'_ (Str), 1 : usize>; // anonymous local - let @6: &'_ (Slice>); // anonymous local - let @7: &'_ (Array, 0 : usize>); // anonymous local - let @8: &'_ (Array, 0 : usize>); // anonymous local - let @9: Array, 0 : usize>; // anonymous local - - @5 := [const ("O no!"); 1 : usize] - @4 := &@5 - @3 := &*(@4) - @2 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@3)) - drop @3 - @9 := core::fmt::rt::{core::fmt::rt::Argument<'a>#1}::none<'_>() - @8 := &@9 - @7 := &*(@8) - @6 := @ArrayToSliceShared<'_, core::fmt::rt::Argument<'_>, 0 : usize>(move (@7)) - drop @7 - @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_v1<'_>(move (@2), move (@6)) - drop @6 + let @4: Array<&'_ (Str), 1 : usize>; // anonymous local + let @5: &'_ (Array, 0 : usize>); // anonymous local + let @6: &'_ (Array, 0 : usize>); // anonymous local + let @7: Array, 0 : usize>; // anonymous local + + @4 := [const ("O no!"); 1 : usize] + @3 := &@4 + @2 := &*(@3) + @7 := core::fmt::rt::{core::fmt::rt::Argument<'a>#1}::none<'_>() + @6 := &@7 + @5 := &*(@6) + @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_v1<'_, 1 : usize, 0 : usize>(move (@2), move (@5)) + drop @5 drop @2 panic(core::panicking::panic_fmt) } @@ -100,33 +91,30 @@ fn test_crate::panic5() let @1: (); // anonymous local let @2: bool; // anonymous local let @3: core::fmt::Arguments<'_>; // anonymous local - let @4: &'_ (Slice<&'_ (Str)>); // anonymous local + let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local let @5: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @6: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @7: Array<&'_ (Str), 1 : usize>; // anonymous local + let @6: Array<&'_ (Str), 1 : usize>; // anonymous local + let @7: (); // anonymous local let @8: (); // anonymous local - let @9: (); // anonymous local @2 := const (false) if move (@2) { nop } else { - @7 := [const ("assert failed"); 1 : usize] - @6 := &@7 - @5 := &*(@6) - @4 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@5)) - drop @5 - @3 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_>(move (@4)) + @6 := [const ("assert failed"); 1 : usize] + @5 := &@6 + @4 := &*(@5) + @3 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_, 1 : usize>(move (@4)) drop @4 panic(core::panicking::panic_fmt) } - @8 := () - @1 := move (@8) + @7 := () + @1 := move (@7) drop @2 drop @1 - @9 := () - @0 := move (@9) + @8 := () + @0 := move (@8) @0 := () return } @@ -142,27 +130,21 @@ fn test_crate::panic7() { let @0: (); // return let @1: core::fmt::Arguments<'_>; // anonymous local - let @2: &'_ (Slice<&'_ (Str)>); // anonymous local + let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: Array<&'_ (Str), 1 : usize>; // anonymous local - let @6: &'_ (Slice>); // anonymous local - let @7: &'_ (Array, 0 : usize>); // anonymous local - let @8: &'_ (Array, 0 : usize>); // anonymous local - let @9: Array, 0 : usize>; // anonymous local - - @5 := [const ("internal error: entered unreachable code: can't reach this"); 1 : usize] - @4 := &@5 - @3 := &*(@4) - @2 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@3)) - drop @3 - @9 := core::fmt::rt::{core::fmt::rt::Argument<'a>#1}::none<'_>() - @8 := &@9 - @7 := &*(@8) - @6 := @ArrayToSliceShared<'_, core::fmt::rt::Argument<'_>, 0 : usize>(move (@7)) - drop @7 - @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_v1<'_>(move (@2), move (@6)) - drop @6 + let @4: Array<&'_ (Str), 1 : usize>; // anonymous local + let @5: &'_ (Array, 0 : usize>); // anonymous local + let @6: &'_ (Array, 0 : usize>); // anonymous local + let @7: Array, 0 : usize>; // anonymous local + + @4 := [const ("internal error: entered unreachable code: can't reach this"); 1 : usize] + @3 := &@4 + @2 := &*(@3) + @7 := core::fmt::rt::{core::fmt::rt::Argument<'a>#1}::none<'_>() + @6 := &@7 + @5 := &*(@6) + @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_v1<'_, 1 : usize, 0 : usize>(move (@2), move (@5)) + drop @5 drop @2 panic(core::panicking::panic_fmt) } diff --git a/charon/tests/ui/params.out b/charon/tests/ui/params.out index a0e048121..249972260 100644 --- a/charon/tests/ui/params.out +++ b/charon/tests/ui/params.out @@ -25,9 +25,9 @@ enum test_crate::E0<'a, 'b, T1, T2> enum test_crate::E1<'a, 'b, T1, T2> where T1 : 'a, - T1 : 'b, - T2 : 'a, T2 : 'b, + T2 : 'a, + T1 : 'b, = | V1(&'a mut (T1), &'b mut (T2)) | V2(alloc::boxed::Box>) @@ -36,9 +36,9 @@ enum test_crate::E1<'a, 'b, T1, T2> enum test_crate::E2<'a, 'b, T1, T2> where T1 : 'a, + T2 : 'b, T1 : 'b, T2 : 'a, - T2 : 'b, = | V1(&'a mut (T1), &'b mut (T2)) | V3(alloc::boxed::Box>) @@ -47,11 +47,11 @@ enum test_crate::E2<'a, 'b, T1, T2> enum test_crate::E3<'a, 'b, 'c, T1, T2> where T1 : 'a, - T1 : 'b, - T1 : 'c, - T2 : 'a, T2 : 'b, + T2 : 'a, + T1 : 'b, T2 : 'c, + T1 : 'c, 'a : 'c, 'b : 'c, = @@ -64,12 +64,12 @@ enum test_crate::E3<'a, 'b, 'c, T1, T2> enum test_crate::E4<'a, 'b, 'c, T1, T2, T3> where T1 : 'a, - T1 : 'b, - T2 : 'a, T2 : 'b, + T2 : 'a, + T1 : 'b, + T3 : 'c, T3 : 'a, T3 : 'b, - T3 : 'c, 'a : 'c, 'b : 'c, = @@ -82,12 +82,12 @@ enum test_crate::E4<'a, 'b, 'c, T1, T2, T3> enum test_crate::E5<'a, 'b, 'c, T1, T2, T3> where T1 : 'a, - T1 : 'b, - T2 : 'a, T2 : 'b, + T2 : 'a, + T1 : 'b, T3 : 'a, - T3 : 'b, T3 : 'c, + T3 : 'b, 'c : 'a, 'c : 'b, = @@ -100,9 +100,9 @@ enum test_crate::E5<'a, 'b, 'c, T1, T2, T3> struct test_crate::S1<'a, 'b, 'c, 'd> where 'c : 'a, - 'c : 'b, - 'd : 'a, 'd : 'b, + 'd : 'a, + 'c : 'b, = { x: test_crate::E1<'a, 'b, &'c mut (u32), &'d (u32)> diff --git a/charon/tests/ui/plain-panic-str.out b/charon/tests/ui/plain-panic-str.out index 350574917..37f60974f 100644 --- a/charon/tests/ui/plain-panic-str.out +++ b/charon/tests/ui/plain-panic-str.out @@ -4,23 +4,20 @@ opaque type core::fmt::Arguments<'a> where 'a : 'a, -fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a>(@1: &'a (Slice<&'static (Str)>)) -> core::fmt::Arguments<'a> +fn core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'a, const N : usize>(@1: &'a (Array<&'static (Str), const N : usize>)) -> core::fmt::Arguments<'a> fn test_crate::main() { let @0: (); // return let @1: core::fmt::Arguments<'_>; // anonymous local - let @2: &'_ (Slice<&'_ (Str)>); // anonymous local + let @2: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local let @3: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @4: &'_ (Array<&'_ (Str), 1 : usize>); // anonymous local - let @5: Array<&'_ (Str), 1 : usize>; // anonymous local + let @4: Array<&'_ (Str), 1 : usize>; // anonymous local - @5 := [const ("O no"); 1 : usize] - @4 := &@5 - @3 := &*(@4) - @2 := @ArrayToSliceShared<'_, &'_ (Str), 1 : usize>(move (@3)) - drop @3 - @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_>(move (@2)) + @4 := [const ("O no"); 1 : usize] + @3 := &@4 + @2 := &*(@3) + @1 := core::fmt::{core::fmt::Arguments<'a>#2}::new_const<'_, 1 : usize>(move (@2)) drop @2 panic(core::panicking::panic_fmt) } diff --git a/charon/tests/ui/polonius_map.out b/charon/tests/ui/polonius_map.out index f6d368467..3f53caad1 100644 --- a/charon/tests/ui/polonius_map.out +++ b/charon/tests/ui/polonius_map.out @@ -101,7 +101,7 @@ impl core::cmp::impls::{impl core::cmp::PartialEq for u32#24} : core::cmp:: fn ne = core::cmp::impls::{impl core::cmp::PartialEq for u32#24}::ne } -impl core::cmp::impls::{impl core::cmp::Eq for u32#41} : core::cmp::Eq +impl core::cmp::impls::{impl core::cmp::Eq for u32#43} : core::cmp::Eq { parent_clause0 = core::cmp::impls::{impl core::cmp::PartialEq for u32#24} } @@ -189,21 +189,21 @@ fn test_crate::get_or_insert<'_0>(@1: &'_0 mut (std::collections::hash::map::Has @6 := const (22 : u32) @5 := &@6 @4 := &*(@5) - @2 := std::collections::hash::map::{std::collections::hash::map::HashMap#2}::get[core::borrow::{impl core::borrow::Borrow for T}, core::hash::impls::{impl core::hash::Hash for u32#11}, core::cmp::impls::{impl core::cmp::Eq for u32#41}, core::cmp::impls::{impl core::cmp::Eq for u32#41}, core::hash::impls::{impl core::hash::Hash for u32#11}, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1}](move (@3), move (@4)) + @2 := std::collections::hash::map::{std::collections::hash::map::HashMap#2}::get[core::borrow::{impl core::borrow::Borrow for T}, core::hash::impls::{impl core::hash::Hash for u32#11}, core::cmp::impls::{impl core::cmp::Eq for u32#43}, core::cmp::impls::{impl core::cmp::Eq for u32#43}, core::hash::impls::{impl core::hash::Hash for u32#11}, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1}](move (@3), move (@4)) drop @4 drop @3 @fake_read(@2) match @2 { 0 => { @9 := &two-phase-mut *(map@1) - @8 := std::collections::hash::map::{std::collections::hash::map::HashMap#2}::insert[core::cmp::impls::{impl core::cmp::Eq for u32#41}, core::hash::impls::{impl core::hash::Hash for u32#11}, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1}](move (@9), const (22 : u32), const (33 : u32)) + @8 := std::collections::hash::map::{std::collections::hash::map::HashMap#2}::insert[core::cmp::impls::{impl core::cmp::Eq for u32#43}, core::hash::impls::{impl core::hash::Hash for u32#11}, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1}](move (@9), const (22 : u32), const (33 : u32)) drop @9 drop @8 @12 := &*(map@1) @15 := const (22 : u32) @14 := &@15 @13 := &*(@14) - @11 := std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap#9}<'_, u32, u32, u32, std::hash::random::RandomState>[core::cmp::impls::{impl core::cmp::Eq for u32#41}, core::hash::impls::{impl core::hash::Hash for u32#11}, core::borrow::{impl core::borrow::Borrow for T}, core::cmp::impls::{impl core::cmp::Eq for u32#41}, core::hash::impls::{impl core::hash::Hash for u32#11}, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1}]::index(move (@12), move (@13)) + @11 := std::collections::hash::map::{impl core::ops::index::Index<&'_0 (Q)> for std::collections::hash::map::HashMap#9}<'_, u32, u32, u32, std::hash::random::RandomState>[core::cmp::impls::{impl core::cmp::Eq for u32#43}, core::hash::impls::{impl core::hash::Hash for u32#11}, core::borrow::{impl core::borrow::Borrow for T}, core::cmp::impls::{impl core::cmp::Eq for u32#43}, core::hash::impls::{impl core::hash::Hash for u32#11}, std::hash::random::{impl core::hash::BuildHasher for std::hash::random::RandomState#1}]::index(move (@12), move (@13)) drop @13 drop @12 @10 := &*(@11) diff --git a/charon/tests/ui/rename_attribute_failure.out b/charon/tests/ui/rename_attribute_failure.out index 4ed9f0843..8894bc0b7 100644 --- a/charon/tests/ui/rename_attribute_failure.out +++ b/charon/tests/ui/rename_attribute_failure.out @@ -36,5 +36,5 @@ error: Error parsing attribute: Unrecognized attribute: `something_else("_Type36 error: aborting due to 6 previous errors -[ ERROR charon_driver:231] The extraction encountered 6 errors +[ ERROR charon_driver:230] The extraction encountered 6 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/string-literal.out b/charon/tests/ui/string-literal.out index 88fe6aad7..9bb5fe00e 100644 --- a/charon/tests/ui/string-literal.out +++ b/charon/tests/ui/string-literal.out @@ -31,11 +31,11 @@ trait alloc::string::ToString fn to_string : alloc::string::ToString::to_string } -fn alloc::string::{impl alloc::string::ToString for Str#47}::to_string<'_0>(@1: &'_0 (Str)) -> alloc::string::String +fn alloc::string::{impl alloc::string::ToString for Str#38}::to_string<'_0>(@1: &'_0 (Str)) -> alloc::string::String -impl alloc::string::{impl alloc::string::ToString for Str#47} : alloc::string::ToString +impl alloc::string::{impl alloc::string::ToString for Str#38} : alloc::string::ToString { - fn to_string = alloc::string::{impl alloc::string::ToString for Str#47}::to_string + fn to_string = alloc::string::{impl alloc::string::ToString for Str#38}::to_string } fn alloc::string::ToString::to_string<'_0, Self>(@1: &'_0 (Self)) -> alloc::string::String @@ -50,7 +50,7 @@ fn test_crate::main() @3 := const ("Hello") @2 := &*(@3) - _s@1 := alloc::string::{impl alloc::string::ToString for Str#47}::to_string(move (@2)) + _s@1 := alloc::string::{impl alloc::string::ToString for Str#38}::to_string(move (@2)) drop @2 @fake_read(_s@1) drop @3 diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out index 54920e908..a468c58e9 100644 --- a/charon/tests/ui/trait-instance-id.out +++ b/charon/tests/ui/trait-instance-id.out @@ -155,9 +155,69 @@ enum core::result::Result = | Err(E) -opaque type core::num::nonzero::NonZeroUsize +trait core::clone::Clone +{ + fn clone : core::clone::Clone::clone + fn clone_from +} + +trait core::marker::Copy +{ + parent_clause_0 : [@TraitClause0]: core::clone::Clone +} + +trait core::num::nonzero::private::Sealed + +trait core::num::nonzero::ZeroablePrimitive +{ + parent_clause_0 : [@TraitClause0]: core::marker::Copy + parent_clause_1 : [@TraitClause1]: core::num::nonzero::private::Sealed + type NonZeroInner + where + [@TraitClause0]: core::marker::Copy, + [@TraitClause1]: core::clone::Clone, +} + +opaque type core::num::nonzero::NonZero + where + [@TraitClause0]: core::num::nonzero::ZeroablePrimitive, + +fn core::clone::impls::{impl core::clone::Clone for usize#5}::clone<'_0>(@1: &'_0 (usize)) -> usize + +impl core::clone::impls::{impl core::clone::Clone for usize#5} : core::clone::Clone +{ + fn clone = core::clone::impls::{impl core::clone::Clone for usize#5}::clone +} -fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::advance_by<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZeroUsize> +impl core::marker::{impl core::marker::Copy for usize#38} : core::marker::Copy +{ + parent_clause0 = core::clone::impls::{impl core::clone::Clone for usize#5} +} + +impl core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} : core::num::nonzero::private::Sealed + +opaque type core::num::nonzero::private::NonZeroUsizeInner + +fn core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}::clone<'_0>(@1: &'_0 (core::num::nonzero::private::NonZeroUsizeInner)) -> core::num::nonzero::private::NonZeroUsizeInner + +impl core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} : core::clone::Clone +{ + fn clone = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}::clone +} + +impl core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27} : core::marker::Copy +{ + parent_clause0 = core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26} +} + +impl core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize#26} : core::num::nonzero::ZeroablePrimitive +{ + parent_clause0 = core::marker::{impl core::marker::Copy for usize#38} + parent_clause1 = core::num::nonzero::{impl core::num::nonzero::private::Sealed for usize#25} + type NonZeroInner = core::num::nonzero::private::NonZeroUsizeInner with [core::num::nonzero::private::{impl core::marker::Copy for core::num::nonzero::private::NonZeroUsizeInner#27}, core::num::nonzero::private::{impl core::clone::Clone for core::num::nonzero::private::NonZeroUsizeInner#26}] +} + +fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::advance_by<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero> unsafe fn core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::__iterator_get_unchecked<'_0, T, const N : usize>(@1: &'_0 mut (core::array::iter::IntoIter), @2: usize) -> core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}::Item @@ -184,67 +244,67 @@ impl core::array::iter::{impl core::iter::traits::collect::I fn core::iter::traits::collect::IntoIterator::into_iter(@1: Self) -> Self::IntoIter -fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}::into_iter(@1: I) -> I +fn core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter(@1: I) -> I where // Inherited clauses: [@TraitClause0]: core::iter::traits::iterator::Iterator, -impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I} : core::iter::traits::collect::IntoIterator +impl core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1} : core::iter::traits::collect::IntoIterator where [@TraitClause0]: core::iter::traits::iterator::Iterator, { type Item = @TraitClause0::Item with [] type IntoIter = I with [@TraitClause0] - fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}::into_iter + fn into_iter = core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}::into_iter } fn core::iter::traits::iterator::Iterator::next<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option fn core::slice::{Slice}::iter<'_0, T>(@1: &'_0 (Slice)) -> core::slice::iter::Iter<'_0, T> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::next<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>)) -> core::option::Option<&'a (T)> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::next<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>)) -> core::option::Option<&'a (T)> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Iter<'a, T>)) -> (usize, core::option::Option) +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Iter<'a, T>)) -> (usize, core::option::Option) -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::count<'a, T>(@1: core::slice::iter::Iter<'a, T>) -> usize +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::count<'a, T>(@1: core::slice::iter::Iter<'a, T>) -> usize -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::option::Option<&'a (T)> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::option::Option<&'a (T)> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::advance_by<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZeroUsize> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::advance_by<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::result::Result<(), core::num::nonzero::NonZero> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::last<'a, T>(@1: core::slice::iter::Iter<'a, T>) -> core::option::Option<&'a (T)> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::last<'a, T>(@1: core::slice::iter::Iter<'a, T>) -> core::option::Option<&'a (T)> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::fold<'a, T, B, F>(@1: core::slice::iter::Iter<'a, T>, @2: B, @3: F) -> B +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::fold<'a, T, B, F>(@1: core::slice::iter::Iter<'a, T>, @2: B, @3: F) -> B where [@TraitClause0]: core::ops::function::FnMut, - (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::fold)))::[@TraitClause0])::Output = B, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#182}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#182}::fold)))::[@TraitClause0])::Output = B, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::for_each<'a, T, F>(@1: core::slice::iter::Iter<'a, T>, @2: F) +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::for_each<'a, T, F>(@1: core::slice::iter::Iter<'a, T>, @2: F) where [@TraitClause0]: core::ops::function::FnMut, - (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::for_each)))::[@TraitClause0])::Output = (), + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#182}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#182}::for_each)))::[@TraitClause0])::Output = (), -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::all<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> bool +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::all<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> bool where [@TraitClause0]: core::ops::function::FnMut, - (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::all)))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#182}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#182}::all)))::[@TraitClause0])::Output = bool, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::any<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> bool +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::any<'a, '_1, T, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> bool where [@TraitClause0]: core::ops::function::FnMut, - (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::any)))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#182}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#182}::any)))::[@TraitClause0])::Output = bool, Unknown decl: 39 -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::find_map<'a, '_1, T, B, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> core::option::Option +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::find_map<'a, '_1, T, B, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> core::option::Option where [@TraitClause0]: core::ops::function::FnMut, - (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::find_map)))::[@TraitClause0])::Output = core::option::Option, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#182}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#182}::find_map)))::[@TraitClause0])::Output = core::option::Option, -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::position<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: P) -> core::option::Option +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::position<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: P) -> core::option::Option where [@TraitClause0]: core::ops::function::FnMut, - (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#181}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#181}::position)))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut#182}<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut) (context: core::slice::iter::{impl#182}::position)))::[@TraitClause0])::Output = bool, trait core::iter::traits::exact_size::ExactSizeIterator { @@ -264,35 +324,35 @@ trait core::iter::traits::double_ended::DoubleEndedIterator fn rfind } -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::rposition<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: P) -> core::option::Option +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::rposition<'a, '_1, T, P>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: P) -> core::option::Option where - [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)>, + [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Item)>, [@TraitClause1]: core::iter::traits::exact_size::ExactSizeIterator>, [@TraitClause2]: core::iter::traits::double_ended::DoubleEndedIterator>, - (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause1]: @TraitDecl5<@Adt2<'_, T>>; [@TraitClause2]: @TraitDecl6<@Adt2<'_, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause1]: @TraitDecl5<@Adt2<'_, T>>; [@TraitClause2]: @TraitDecl6<@Adt2<'_, T>>) (context: core::slice::iter::{impl#181}::rposition)))::[@TraitClause0])::Output = bool, + (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause1]: @TraitDecl9<@Adt2<'_, T>>; [@TraitClause2]: @TraitDecl10<@Adt2<'_, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Item)>; [@TraitClause1]: @TraitDecl9<@Adt2<'_, T>>; [@TraitClause2]: @TraitDecl10<@Adt2<'_, T>>) (context: core::slice::iter::{impl#182}::rposition)))::[@TraitClause0])::Output = bool, -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}<'_, T>::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}<'_, T>::Item Unknown decl: 44 -impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}<'a, T> : core::iter::traits::iterator::Iterator> +impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}<'a, T> : core::iter::traits::iterator::Iterator> { type Item = &'a (T) with [] - fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::next - fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::size_hint - fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::count - fn nth = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::nth - fn advance_by = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::advance_by - fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::last - fn fold = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::fold - fn for_each = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::for_each - fn all = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::all - fn any = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::any + fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::next + fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::size_hint + fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::count + fn nth = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::nth + fn advance_by = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::advance_by + fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::last + fn fold = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::fold + fn for_each = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::for_each + fn all = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::all + fn any = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::any fn find = @Fun39 - fn find_map = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::find_map - fn position = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::position - fn rposition = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::rposition - fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}::__iterator_get_unchecked + fn find_map = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::find_map + fn position = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::position + fn rposition = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::rposition + fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}::__iterator_get_unchecked fn is_sorted_by = @Fun44 } @@ -301,63 +361,63 @@ trait core::ops::arith::AddAssign fn add_assign : core::ops::arith::AddAssign::add_assign } -fn core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#319}::add_assign<'_0, '_1, '_2>(@1: &'_1 mut (i32), @2: &'_2 (i32)) +fn core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#365}::add_assign<'_0, '_1, '_2>(@1: &'_1 mut (i32), @2: &'_2 (i32)) -impl<'_0> core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#319}<'_0> : core::ops::arith::AddAssign +impl<'_0> core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#365}<'_0> : core::ops::arith::AddAssign { - fn add_assign = core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#319}::add_assign + fn add_assign = core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#365}::add_assign } fn core::ops::arith::AddAssign::add_assign<'_0, Self, Rhs>(@1: &'_0 mut (Self), @2: Rhs) fn core::slice::{Slice}::chunks<'_0, T>(@1: &'_0 (Slice), @2: usize) -> core::slice::iter::Chunks<'_0, T> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::next<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>)) -> core::option::Option<&'a (Slice)> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::next<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>)) -> core::option::Option<&'a (Slice)> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Chunks<'a, T>)) -> (usize, core::option::Option) +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::Chunks<'a, T>)) -> (usize, core::option::Option) -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::count<'a, T>(@1: core::slice::iter::Chunks<'a, T>) -> usize +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::count<'a, T>(@1: core::slice::iter::Chunks<'a, T>) -> usize -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>), @2: usize) -> core::option::Option#70}<'_, T>::Item> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>), @2: usize) -> core::option::Option#71}<'_, T>::Item> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>) -> core::option::Option#70}<'_, T>::Item> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::last<'a, T>(@1: core::slice::iter::Chunks<'a, T>) -> core::option::Option#71}<'_, T>::Item> -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}<'_, T>::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Chunks<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}<'_, T>::Item -impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}<'a, T> : core::iter::traits::iterator::Iterator> +impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}<'a, T> : core::iter::traits::iterator::Iterator> { type Item = &'a (Slice) with [] - fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::next - fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::size_hint - fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::count - fn nth = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::nth - fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::last - fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}::__iterator_get_unchecked + fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::next + fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::size_hint + fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::count + fn nth = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::nth + fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::last + fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}::__iterator_get_unchecked } fn core::slice::{Slice}::chunks_exact<'_0, T>(@1: &'_0 (Slice), @2: usize) -> core::slice::iter::ChunksExact<'_0, T> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::next<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>)) -> core::option::Option<&'a (Slice)> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::next<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>)) -> core::option::Option<&'a (Slice)> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::ChunksExact<'a, T>)) -> (usize, core::option::Option) +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::size_hint<'a, '_1, T>(@1: &'_1 (core::slice::iter::ChunksExact<'a, T>)) -> (usize, core::option::Option) -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::count<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>) -> usize +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::count<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>) -> usize -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>), @2: usize) -> core::option::Option#89}<'_, T>::Item> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::nth<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>), @2: usize) -> core::option::Option#90}<'_, T>::Item> -fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::last<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>) -> core::option::Option#89}<'_, T>::Item> +fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::last<'a, T>(@1: core::slice::iter::ChunksExact<'a, T>) -> core::option::Option#90}<'_, T>::Item> -unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}<'_, T>::Item +unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::ChunksExact<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}<'_, T>::Item -impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}<'a, T> : core::iter::traits::iterator::Iterator> +impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}<'a, T> : core::iter::traits::iterator::Iterator> { type Item = &'a (Slice) with [] - fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::next - fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::size_hint - fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::count - fn nth = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::nth - fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::last - fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}::__iterator_get_unchecked + fn next = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::next + fn size_hint = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::size_hint + fn count = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::count + fn nth = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::nth + fn last = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::last + fn __iterator_get_unchecked = core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}::__iterator_get_unchecked } fn test_crate::main() @@ -450,7 +510,7 @@ fn test_crate::main() @6 := copy (a@1) @5 := core::array::iter::{impl core::iter::traits::collect::IntoIterator for Array}::into_iter(move (@6)) drop @6 - @4 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}]::into_iter(move (@5)) + @4 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::array::iter::{impl core::iter::traits::iterator::Iterator for core::array::iter::IntoIter#2}]::into_iter(move (@5)) drop @5 @fake_read(@4) iter@7 := move (@4) @@ -475,14 +535,14 @@ fn test_crate::main() drop @12 drop @10 drop @9 - @68 := () - @8 := move (@68) + @67 := () + @8 := move (@67) continue 0 } } } - @67 := () - @3 := move (@67) + @68 := () + @3 := move (@68) drop @12 drop @10 drop @9 @@ -496,14 +556,14 @@ fn test_crate::main() drop @19 @17 := core::slice::{Slice}::iter(move (@18)) drop @18 - @16 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}<'_, i32>]::into_iter(move (@17)) + @16 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}<'_, i32>]::into_iter(move (@17)) drop @17 @fake_read(@16) iter@20 := move (@16) loop { @24 := &mut iter@20 @23 := &two-phase-mut *(@24) - @22 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#181}<'_, i32>::next(move (@23)) + @22 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>#182}<'_, i32>::next(move (@23)) drop @23 @fake_read(@22) match @22 { @@ -514,7 +574,7 @@ fn test_crate::main() v@25 := copy ((@22 as variant @1).0) @27 := &two-phase-mut i@2 @28 := copy (v@25) - @26 := core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#319}<'_>::add_assign(move (@27), move (@28)) + @26 := core::ops::arith::{impl core::ops::arith::AddAssign<&'_0 (i32)> for i32#365}<'_>::add_assign(move (@27), move (@28)) drop @28 drop @27 drop @26 @@ -543,14 +603,14 @@ fn test_crate::main() drop @33 @31 := core::slice::{Slice}::chunks(move (@32), const (2 : usize)) drop @32 - @30 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}<'_, i32>]::into_iter(move (@31)) + @30 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}<'_, i32>]::into_iter(move (@31)) drop @31 @fake_read(@30) iter@34 := move (@30) loop { @38 := &mut iter@34 @37 := &two-phase-mut *(@38) - @36 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#70}<'_, i32>::next(move (@37)) + @36 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Chunks<'a, T>#71}<'_, i32>::next(move (@37)) drop @37 @fake_read(@36) match @36 { @@ -564,14 +624,14 @@ fn test_crate::main() drop @38 drop @36 drop @35 - @74 := () - @8 := move (@74) + @73 := () + @8 := move (@73) continue 0 } } } - @73 := () - @29 := move (@73) + @74 := () + @29 := move (@74) drop @38 drop @36 drop @35 @@ -583,14 +643,14 @@ fn test_crate::main() drop @43 @41 := core::slice::{Slice}::chunks_exact(move (@42), const (2 : usize)) drop @42 - @40 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I}>[core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}<'_, i32>]::into_iter(move (@41)) + @40 := core::iter::traits::collect::{impl core::iter::traits::collect::IntoIterator for I#1}>[core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}<'_, i32>]::into_iter(move (@41)) drop @41 @fake_read(@40) iter@44 := move (@40) loop { @48 := &mut iter@44 @47 := &two-phase-mut *(@48) - @46 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#89}<'_, i32>::next(move (@47)) + @46 := core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::ChunksExact<'a, T>#90}<'_, i32>::next(move (@47)) drop @47 @fake_read(@46) match @46 { @@ -604,14 +664,14 @@ fn test_crate::main() drop @48 drop @46 drop @45 - @77 := () - @8 := move (@77) + @76 := () + @8 := move (@76) continue 0 } } } - @76 := () - @39 := move (@76) + @77 := () + @39 := move (@77) drop @48 drop @46 drop @45 @@ -669,6 +729,8 @@ fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2 fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> Self::Output +fn core::clone::Clone::clone<'_0, Self>(@1: &'_0 (Self)) -> Self + fn core::iter::traits::double_ended::DoubleEndedIterator::next_back<'_0, Self>(@1: &'_0 mut (Self)) -> core::option::Option<(parents(Self)::[@TraitClause0])::Item> diff --git a/charon/tests/ui/unsupported/issue-165-vec-macro.out b/charon/tests/ui/unsupported/issue-165-vec-macro.out index 2b350d429..8b270a0ce 100644 --- a/charon/tests/ui/unsupported/issue-165-vec-macro.out +++ b/charon/tests/ui/unsupported/issue-165-vec-macro.out @@ -6,7 +6,7 @@ error: Nullary operations are not supported | = note: this error originates in the macro `vec` (in Nightly builds, run with -Z macro-backtrace for more info) -error: aborting due to previous error +error: aborting due to 1 previous error -[ ERROR charon_driver:231] The extraction encountered 1 errors +[ ERROR charon_driver:230] The extraction encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/projection-index-from-end.out b/charon/tests/ui/unsupported/projection-index-from-end.out index fc28cb565..d42f5898f 100644 --- a/charon/tests/ui/unsupported/projection-index-from-end.out +++ b/charon/tests/ui/unsupported/projection-index-from-end.out @@ -4,7 +4,7 @@ error: Unexpected ProjectionElem::ConstantIndex 4 | [.., _named] => (), | ^^^^^^ -error: aborting due to previous error +error: aborting due to 1 previous error -[ ERROR charon_driver:231] The extraction encountered 1 errors +[ ERROR charon_driver:230] The extraction encountered 1 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/unbound-lifetime.out b/charon/tests/ui/unsupported/unbound-lifetime.out index 0a7cd7f14..a8910f71c 100644 --- a/charon/tests/ui/unsupported/unbound-lifetime.out +++ b/charon/tests/ui/unsupported/unbound-lifetime.out @@ -27,5 +27,5 @@ error: Ignoring the following item due to an error: test_crate::get error: aborting due to 3 previous errors For more information about this error, try `rustc --explain E0261`. -[ ERROR charon_driver:231] The extraction encountered 2 errors +[ ERROR charon_driver:230] The extraction encountered 2 errors Error: Charon driver exited with code 1 diff --git a/charon/tests/ui/unsupported/well-formedness-bound.out b/charon/tests/ui/unsupported/well-formedness-bound.out index d45e26bfa..cff7a03c8 100644 --- a/charon/tests/ui/unsupported/well-formedness-bound.out +++ b/charon/tests/ui/unsupported/well-formedness-bound.out @@ -1,4 +1,4 @@ -error: Unsupported clause: WellFormed(Type(Ref(Region { kind: ReEarlyParam(EarlyParamRegion { def_id: DefId { krate: "test_crate", path: [DisambiguatedDefPathItem { data: ValueNs("get"), disambiguator: 0 }, DisambiguatedDefPathItem { data: LifetimeNs("'a"), disambiguator: 0 }], index: (0, 4) }, index: 0, name: "'a" }) }, Tuple([]), false))) +error: Unsupported clause: WellFormed(Type(Ref(Region { kind: ReEarlyParam(EarlyParamRegion { index: 0, name: "'a" }) }, Tuple([]), false))) --> tests/ui/unsupported/well-formedness-bound.rs:4:5 | 4 | &'a ():, @@ -14,5 +14,5 @@ error: Ignoring the following item due to an error: test_crate::get error: aborting due to 2 previous errors -[ ERROR charon_driver:231] The extraction encountered 2 errors +[ ERROR charon_driver:230] The extraction encountered 2 errors Error: Charon driver exited with code 1 diff --git a/flake.lock b/flake.lock index 95d20de5e..4b5fda2ff 100644 --- a/flake.lock +++ b/flake.lock @@ -79,19 +79,16 @@ }, "rust-overlay": { "inputs": { - "flake-utils": [ - "flake-utils" - ], "nixpkgs": [ "nixpkgs" ] }, "locked": { - "lastModified": 1701656211, - "narHash": "sha256-lfFXsLWH4hVbEKR6K+UcDiKxeS6Lz4FkC1DZ9LHqf9Y=", + "lastModified": 1719368303, + "narHash": "sha256-vhkKOUs9eOZgcPrA6wMw7a7J48pEjVuhzQfitVwVv1g=", "owner": "oxalica", "repo": "rust-overlay", - "rev": "47a276e820ae4ae1b8d98a503bf09d2ceb52dfd8", + "rev": "32415b22fd3b454e4a1385af64aa5cef9766ff4c", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 3efb840af..8185d0def 100644 --- a/flake.nix +++ b/flake.nix @@ -7,7 +7,6 @@ nixpkgs.url = "nixpkgs/nixos-unstable"; rust-overlay = { url = "github:oxalica/rust-overlay"; - inputs.flake-utils.follows = "flake-utils"; inputs.nixpkgs.follows = "nixpkgs"; }; crane = { diff --git a/rust-toolchain b/rust-toolchain index 94321c67a..5e72e4a89 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2023-11-16" +channel = "nightly-2024-06-25" components = [ "rustc-dev", "llvm-tools-preview" ]