From 6dfe1fd89ace83a47087bd54d61dfc759f3fcf50 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurel=20B=C3=ADl=C3=BD?= Date: Mon, 10 Jan 2022 10:56:03 +0100 Subject: [PATCH] Update rustc to nightly-2022-01-13 --- Cargo.lock | 348 ++++++++---------- .../domains/definitely_accessible/state.rs | 13 +- prusti-interface/src/environment/mod.rs | 6 +- prusti-specs/src/specifications/common.rs | 1 + prusti-specs/src/specifications/untyped.rs | 12 +- .../cargo_verify/prusti_toml/output.stdout | 2 +- .../tests/parse/ui/after_expiry.stdout | 8 +- prusti-tests/tests/parse/ui/and.stdout | 10 +- prusti-tests/tests/parse/ui/composite.stdout | 42 +-- prusti-tests/tests/parse/ui/exists.stdout | 12 +- prusti-tests/tests/parse/ui/expression.stdout | 4 +- prusti-tests/tests/parse/ui/forall.stdout | 12 +- prusti-tests/tests/parse/ui/implies.stdout | 10 +- .../parse/ui/predicates-visibility.stdout | 2 +- prusti-tests/tests/parse/ui/predicates.stdout | 4 +- .../tests/parse/ui/spec_entailment.stdout | 8 +- .../tests/parse/ui/trait-bounds.stdout | 4 +- prusti-tests/tests/parse/ui/traits.stdout | 12 +- prusti-tests/tests/parse/ui/true.stdout | 4 +- .../typecheck/ui/forall_encode_typeck.stdout | 4 +- .../tests/typecheck/ui/forall_triggers.stdout | 16 +- .../tests/typecheck/ui/nested_forall.stdout | 12 +- prusti-tests/tests/verify/ui/collect.stdout | 4 +- prusti-tests/tests/verify/ui/false.stdout | 2 +- .../tests/verify/ui/forall_verify.stdout | 12 +- prusti-tests/tests/verify/ui/predicate.stdout | 4 +- prusti-tests/tests/verify/ui/pure.stdout | 2 +- .../src/encoder/counterexample_translation.rs | 6 +- .../src/encoder/mir/procedures/encoder.rs | 3 +- .../src/encoder/mir/pure/interpreter/mod.rs | 8 +- .../mir/pure/pure_functions/interpreter.rs | 18 +- prusti-viper/src/encoder/mir/types/encoder.rs | 7 +- .../src/encoder/mir/types/interface.rs | 2 +- prusti-viper/src/encoder/mir_encoder/mod.rs | 6 +- prusti-viper/src/encoder/procedure_encoder.rs | 43 +-- prusti-viper/src/encoder/snapshot/encoder.rs | 10 +- rust-toolchain | 2 +- 37 files changed, 319 insertions(+), 356 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index b841f3660d6..a7cc226baf2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -34,7 +34,7 @@ dependencies = [ "env_logger", "glob", "log", - "serde 1.0.131", + "serde 1.0.133", "serde_json", "syn", ] @@ -50,9 +50,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.51" +version = "1.0.52" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8b26702f315f53b6071259e15dd9d64528213b44d61de1ec926eca7715d62203" +checksum = "84450d0b4a8bd1ba4144ce8ce718fbc5d071358b1e5384bace6536b3d1f2d5b3" [[package]] name = "arrayvec" @@ -131,14 +131,14 @@ version = "1.3.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b1f45e9417d87227c7a56d22e471c6206462cba514c7590c09aff4cf6d1ddcad" dependencies = [ - "serde 1.0.131", + "serde 1.0.133", ] [[package]] name = "bitflags" -version = "1.3.2" +version = "1.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" +checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693" [[package]] name = "block-buffer" @@ -158,7 +158,7 @@ dependencies = [ "lazy_static", "memchr", "regex-automata", - "serde 1.0.131", + "serde 1.0.133", ] [[package]] @@ -173,9 +173,9 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.8.0" +version = "3.9.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f1e260c3a9040a7c19a12468758f4c16f31a81a1fe087482be9570ec864bb6c" +checksum = "a4a45a46ab1f2412e53d3a0ade76ffad2025804294569aae387231a0cd6e0899" [[package]] name = "byteorder" @@ -198,12 +198,12 @@ checksum = "c4872d67bab6358e59559027aa3b9157c53d9358c51423c17554809a8858e0f8" [[package]] name = "cargo-test-macro" version = "0.1.0" -source = "git+https://github.com/rust-lang/cargo.git#da8dd70c5c5b397322c8ef5a1ba891d7e7fe5be8" +source = "git+https://github.com/rust-lang/cargo.git#e77c0719fd496eb98b1bbdcaf35f415b0ffcc555" [[package]] name = "cargo-test-support" version = "0.1.0" -source = "git+https://github.com/rust-lang/cargo.git#da8dd70c5c5b397322c8ef5a1ba891d7e7fe5be8" +source = "git+https://github.com/rust-lang/cargo.git#e77c0719fd496eb98b1bbdcaf35f415b0ffcc555" dependencies = [ "anyhow", "cargo-test-macro", @@ -225,7 +225,7 @@ dependencies = [ [[package]] name = "cargo-util" version = "0.1.2" -source = "git+https://github.com/rust-lang/cargo.git#da8dd70c5c5b397322c8ef5a1ba891d7e7fe5be8" +source = "git+https://github.com/rust-lang/cargo.git#e77c0719fd496eb98b1bbdcaf35f415b0ffcc555" dependencies = [ "anyhow", "core-foundation", @@ -317,9 +317,9 @@ dependencies = [ [[package]] name = "combine" -version = "4.6.2" +version = "4.6.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b2b2f5d0ee456f3928812dfc8c6d9a1d592b98678f6d56db9b0cd2b7bc6c8db5" +checksum = "50b727aacc797f9fc28e355d21f34709ac4fc9adecfe470ad07b8f4464f53062" dependencies = [ "bytes 1.1.0", "memchr", @@ -358,7 +358,7 @@ dependencies = [ "miow 0.3.7", "regex", "rustfix", - "serde 1.0.131", + "serde 1.0.133", "serde_derive", "serde_json", "tester", @@ -374,7 +374,7 @@ dependencies = [ "lazy_static", "nom", "rust-ini", - "serde 1.0.131", + "serde 1.0.133", "serde-hjson", "serde_json", "toml", @@ -423,9 +423,9 @@ dependencies = [ [[package]] name = "crossbeam-channel" -version = "0.5.1" +version = "0.5.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "06ed27e177f16d65f0f0c22a213e17c696ace5dd64b14258b52f9417ccb52db4" +checksum = "e54ea8bc3fb1ee042f5aace6e3c6e025d3874866da222930f70ce62aceba0bfa" dependencies = [ "cfg-if 1.0.0", "crossbeam-utils", @@ -444,9 +444,9 @@ dependencies = [ [[package]] name = "crossbeam-epoch" -version = "0.9.5" +version = "0.9.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4ec02e091aa634e2c3ada4a392989e7c3116673ef0ac5b72232439094d73b7fd" +checksum = "97242a70df9b89a65d0b6df3c4bf5b9ce03c5b7309019777fbde37e7537f8762" dependencies = [ "cfg-if 1.0.0", "crossbeam-utils", @@ -457,9 +457,9 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.5" +version = "0.8.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d82cfc11ce7f2c3faef78d8a684447b40d503d9681acebed6cb728d45940c4db" +checksum = "cfcae03edb34f947e64acdb1c33ec169824e20657e9ecb61cef6c8c74dcb8120" dependencies = [ "cfg-if 1.0.0", "lazy_static", @@ -487,7 +487,7 @@ dependencies = [ "csv-core", "itoa 0.4.8", "ryu", - "serde 1.0.131", + "serde 1.0.133", ] [[package]] @@ -505,7 +505,7 @@ version = "3.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a19c6cedffdc8c03a3346d723eb20bd85a13362bb96dc2ac000842c6381ec7bf" dependencies = [ - "nix 0.23.0", + "nix 0.23.1", "winapi 0.3.9", ] @@ -641,6 +641,15 @@ dependencies = [ "synstructure", ] +[[package]] +name = "fastrand" +version = "1.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "779d043b6a0b90cc4c0ed7ee380a6504394cee7efd7db050e3774eee387324b2" +dependencies = [ + "instant", +] + [[package]] name = "filetime" version = "0.2.15" @@ -731,9 +740,9 @@ checksum = "3dcaa9ae7725d12cdb85b3ad99a434db70b468c09ded17e012d86b5c1010f7a7" [[package]] name = "futures" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a12aa0eb539080d55c3f2d45a67c3b58b6b0773c1a3ca2dfec66d58c97fd66ca" +checksum = "28560757fe2bb34e79f907794bb6b22ae8b0e5c669b638a1132f2592b19035b4" dependencies = [ "futures-channel", "futures-core", @@ -745,9 +754,9 @@ dependencies = [ [[package]] name = "futures-channel" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5da6ba8c3bb3c165d3c7319fc1cc8304facf1fb8db99c5de877183c08a273888" +checksum = "ba3dda0b6588335f360afc675d0564c17a77a2bda81ca178a4b6081bd86c7f0b" dependencies = [ "futures-core", "futures-sink", @@ -755,24 +764,22 @@ dependencies = [ [[package]] name = "futures-core" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "88d1c26957f23603395cd326b0ffe64124b818f4449552f960d815cfba83a53d" +checksum = "d0c8ff0461b82559810cdccfde3215c3f373807f5e5232b71479bff7bb2583d7" [[package]] name = "futures-io" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "522de2a0fe3e380f1bc577ba0474108faf3f6b18321dbf60b3b9c39a75073377" +checksum = "b1f9d34af5a1aac6fb380f735fe510746c38067c5bf16c7fd250280503c971b2" [[package]] name = "futures-macro" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18e4a4b95cea4b4ccbcf1c5675ca7c4ee4e9e75eb79944d07defde18068f79bb" +checksum = "6dbd947adfffb0efc70599b3ddcf7b5597bb5fa9e245eb99f62b3a5f7bb8bd3c" dependencies = [ - "autocfg", - "proc-macro-hack", "proc-macro2", "quote", "syn", @@ -780,39 +787,36 @@ dependencies = [ [[package]] name = "futures-sink" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36ea153c13024fe480590b3e3d4cad89a0cfacecc24577b68f86c6ced9c2bc11" +checksum = "e3055baccb68d74ff6480350f8d6eb8fcfa3aa11bdc1a1ae3afdd0514617d508" [[package]] name = "futures-task" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1d3d00f4eddb73e498a54394f228cd55853bdf059259e8e7bc6e69d408892e99" +checksum = "6ee7c6485c30167ce4dfb83ac568a849fe53274c831081476ee13e0dce1aad72" [[package]] name = "futures-util" -version = "0.3.17" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36568465210a3a6ee45e1f165136d68671471a501e632e9a98d96872222b5481" +checksum = "d9b5cf40b47a271f77a8b1bec03ca09044d99d2372c0de244e66430761127164" dependencies = [ - "autocfg", "futures-core", "futures-macro", "futures-sink", "futures-task", - "pin-project-lite 0.2.7", + "pin-project-lite 0.2.8", "pin-utils", - "proc-macro-hack", - "proc-macro-nested", "slab", ] [[package]] name = "generic-array" -version = "0.14.4" +version = "0.14.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "501466ecc8a30d1d3b7fc9229b122b2ce8ed6e9d9223f1138d4babb253e51817" +checksum = "fd48d33ec7f05fbfa152300fdad764757cbded343c1aa1cff2fbaf4134851803" dependencies = [ "typenum", "version_check", @@ -950,13 +954,13 @@ checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" [[package]] name = "http" -version = "0.2.5" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1323096b05d41827dadeaee54c9981958c0f94e670bc94ed80037d1a7b8b186b" +checksum = "31f4c6746584866f0feabcc69893c5b51beef3831656a968ed7ae254cdc4fd03" dependencies = [ "bytes 1.1.0", "fnv", - "itoa 0.4.8", + "itoa 1.0.1", ] [[package]] @@ -1009,7 +1013,7 @@ dependencies = [ "httparse", "httpdate 0.3.2", "itoa 0.4.8", - "pin-project 1.0.8", + "pin-project 1.0.10", "socket2", "tokio 0.2.25", "tower-service", @@ -1047,14 +1051,14 @@ version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "74086667896a940438f2118212f313abba4aff3831fef6f4b17d02add5c8bb60" dependencies = [ - "serde 1.0.131", + "serde 1.0.133", ] [[package]] name = "indexmap" -version = "1.7.0" +version = "1.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bc633605454125dec4b66843673f01c7df2b89479b32e0ed634e43a91cff62a5" +checksum = "282a6247722caba404c065016bbfa522806e51714c34f5dfc3e4a3a46fcb4223" dependencies = [ "autocfg", "hashbrown", @@ -1069,6 +1073,15 @@ dependencies = [ "bytes 0.5.6", ] +[[package]] +name = "instant" +version = "0.1.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7a5bbe824c507c5da5956355e86a746d82e0e1464f65d862cc5e71da70e94b2c" +dependencies = [ + "cfg-if 1.0.0", +] + [[package]] name = "iovec" version = "0.1.4" @@ -1391,21 +1404,22 @@ dependencies = [ [[package]] name = "nix" -version = "0.20.0" +version = "0.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa9b4819da1bc61c0ea48b63b7bc8604064dd43013e7cc325df098d49cd7c18a" +checksum = "f5e06129fb611568ef4e868c14b326274959aa70ff7776e9d55323531c374945" dependencies = [ "bitflags", "cc", "cfg-if 1.0.0", "libc", + "memoffset", ] [[package]] name = "nix" -version = "0.23.0" +version = "0.23.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f305c2c2e4c39a82f7bf0bf65fb557f9070ce06781d4f2454295cc34b1c43188" +checksum = "9f866317acbd3a240710c63f065ffb1e4fd466259045ccb504130b7f668f35c6" dependencies = [ "bitflags", "cc", @@ -1464,9 +1478,9 @@ dependencies = [ [[package]] name = "num_cpus" -version = "1.13.0" +version = "1.13.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "05499f3756671c15885fee9034446956fff3f243d6077b91e5767df161f766b3" +checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1" dependencies = [ "hermit-abi", "libc", @@ -1509,9 +1523,9 @@ dependencies = [ [[package]] name = "openssl-probe" -version = "0.1.4" +version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28988d872ab76095a6e6ac88d99b54fd267702734fd7ffe610ca27f533ddb95a" +checksum = "ff011a302c396a5197692431fc1948019154afc178baf7d8e37367442a4601cf" [[package]] name = "openssl-sys" @@ -1534,27 +1548,27 @@ checksum = "d4fd5641d01c8f18a23da7b6fe29298ff4b55afcccdf78973b24cf3175fee32e" [[package]] name = "pin-project" -version = "0.4.28" +version = "0.4.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "918192b5c59119d51e0cd221f4d49dde9112824ba717369e903c97d076083d0f" +checksum = "9615c18d31137579e9ff063499264ddc1278e7b1982757ebc111028c4d1dc909" dependencies = [ - "pin-project-internal 0.4.28", + "pin-project-internal 0.4.29", ] [[package]] name = "pin-project" -version = "1.0.8" +version = "1.0.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "576bc800220cc65dac09e99e97b08b358cfab6e17078de8dc5fee223bd2d0c08" +checksum = "58ad3879ad3baf4e44784bc6a718a8698867bb991f8ce24d1bcbe2cfb4c3a75e" dependencies = [ - "pin-project-internal 1.0.8", + "pin-project-internal 1.0.10", ] [[package]] name = "pin-project-internal" -version = "0.4.28" +version = "0.4.29" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3be26700300be6d9d23264c73211d8190e755b6b5ca7a1b28230025511b52a5e" +checksum = "044964427019eed9d49d9d5bbce6047ef18f37100ea400912a9fa4a3523ab12a" dependencies = [ "proc-macro2", "quote", @@ -1563,9 +1577,9 @@ dependencies = [ [[package]] name = "pin-project-internal" -version = "1.0.8" +version = "1.0.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6e8fe8163d14ce7f0cdac2e040116f22eac817edabff0be91e8aff7e9accf389" +checksum = "744b6f092ba29c3650faf274db506afd39944f48420f6c86b17cfe0ee1cb36bb" dependencies = [ "proc-macro2", "quote", @@ -1580,9 +1594,9 @@ checksum = "257b64915a082f7811703966789728173279bdebb956b143dbcd23f6f970a777" [[package]] name = "pin-project-lite" -version = "0.2.7" +version = "0.2.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8d31d11c69a6b52a174b42bdc0c30e5e11670f90788b2c471c31c1d17d449443" +checksum = "e280fbe77cc62c91527259e9442153f4688736748d24660126286329742b4c6c" [[package]] name = "pin-utils" @@ -1598,27 +1612,15 @@ checksum = "58893f751c9b0412871a09abd62ecd2a00298c6c83befa223ef98c52aef40cbe" [[package]] name = "ppv-lite86" -version = "0.2.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ed0cfbc8191465bed66e1718596ee0b0b35d5ee1f41c5df2189d0fe8bde535ba" - -[[package]] -name = "proc-macro-hack" -version = "0.5.19" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dbf0c48bc1d91375ae5c3cd81e3722dff1abcf81a30960240640d223f59fe0e5" - -[[package]] -name = "proc-macro-nested" -version = "0.1.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bc881b2c22681370c6a780e47af9840ef841837bc98118431d4e1868bd0c1086" +checksum = "eb9f9e6e233e5c4a35559a617bf40a4ec447db2e84c20b55a6f83167b7e57872" [[package]] name = "proc-macro2" -version = "1.0.34" +version = "1.0.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2f84e92c0f7c9d58328b85a78557813e4bd845130db68d7184635344399423b1" +checksum = "c7342d5883fbccae1cc37a2353b09c87c9b0f3afd73f5fb9bba687a1f733b029" dependencies = [ "unicode-xid", ] @@ -1649,7 +1651,7 @@ dependencies = [ "log", "prusti-utils", "regex", - "serde 1.0.131", + "serde 1.0.133", "uuid", "viper", "vir", @@ -1691,7 +1693,7 @@ dependencies = [ "prusti-utils", "regex", "rustc-hash", - "serde 1.0.131", + "serde 1.0.133", "vir", ] @@ -1701,8 +1703,8 @@ version = "0.1.0" dependencies = [ "ctrlc", "glob", - "nix 0.23.0", - "serde 1.0.131", + "nix 0.23.1", + "serde 1.0.133", "toml", "walkdir", ] @@ -1719,7 +1721,7 @@ dependencies = [ "num_cpus", "prusti-common", "reqwest", - "serde 1.0.131", + "serde 1.0.133", "tokio 0.2.25", "url", "viper", @@ -1733,7 +1735,7 @@ dependencies = [ "proc-macro2", "prusti-utils", "quote", - "serde 1.0.131", + "serde 1.0.133", "serde_json", "syn", "uuid", @@ -1768,7 +1770,7 @@ dependencies = [ "prusti-specs", "regex", "rustc-hash", - "serde 1.0.131", + "serde 1.0.133", "viper", "vir", ] @@ -1781,9 +1783,9 @@ checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0" [[package]] name = "quote" -version = "1.0.10" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "38bc8cc6a5f2e3655e0899c1b848643b2562f853f114bfec7be120678e3ace05" +checksum = "47aa80447ce4daf1717500037052af176af5d38cc3e571d9ec1c7353fc10c87d" dependencies = [ "proc-macro2", ] @@ -1809,21 +1811,9 @@ checksum = "6a6b1679d49b24bbfe0c803429aa1874472f50d9b363131f0e89fc356b544d03" dependencies = [ "getrandom 0.1.16", "libc", - "rand_chacha 0.2.2", + "rand_chacha", "rand_core 0.5.1", - "rand_hc 0.2.0", -] - -[[package]] -name = "rand" -version = "0.8.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2e7573632e6454cf6b99d7aac4ccca54be06da05aca2ef7423d22d27d4d4bcd8" -dependencies = [ - "libc", - "rand_chacha 0.3.1", - "rand_core 0.6.3", - "rand_hc 0.3.1", + "rand_hc", ] [[package]] @@ -1836,16 +1826,6 @@ dependencies = [ "rand_core 0.5.1", ] -[[package]] -name = "rand_chacha" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" -dependencies = [ - "ppv-lite86", - "rand_core 0.6.3", -] - [[package]] name = "rand_core" version = "0.3.1" @@ -1870,15 +1850,6 @@ dependencies = [ "getrandom 0.1.16", ] -[[package]] -name = "rand_core" -version = "0.6.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d34f1408f55294453790c48b2f1ebbb1c5b4b7563eb1f418bcfcfdbb06ebb4e7" -dependencies = [ - "getrandom 0.2.3", -] - [[package]] name = "rand_hc" version = "0.2.0" @@ -1888,15 +1859,6 @@ dependencies = [ "rand_core 0.5.1", ] -[[package]] -name = "rand_hc" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d51e9f596de227fda2ea6c84607f5558e196eeaf43c986b724ba4fb8fdf497e7" -dependencies = [ - "rand_core 0.6.3", -] - [[package]] name = "rayon" version = "1.5.1" @@ -2018,8 +1980,8 @@ dependencies = [ "mime_guess", "native-tls", "percent-encoding", - "pin-project-lite 0.2.7", - "serde 1.0.131", + "pin-project-lite 0.2.8", + "serde 1.0.133", "serde_json", "serde_urlencoded 0.7.0", "tokio 0.2.25", @@ -2081,7 +2043,7 @@ checksum = "f2c50b74badcddeb8f7652fa8323ce440b95286f8e4b64ebfd871c609672704e" dependencies = [ "anyhow", "log", - "serde 1.0.131", + "serde 1.0.133", "serde_json", ] @@ -2120,16 +2082,16 @@ dependencies = [ "http", "lazy_static", "log", - "nix 0.20.0", + "nix 0.20.2", "percent-encoding", "remove_dir_all 0.7.0", "scopeguard", - "serde 1.0.131", + "serde 1.0.133", "serde_json", "tar", "tempfile", "thiserror", - "tokio 1.14.0", + "tokio 1.15.0", "tokio-stream", "toml", "walkdir", @@ -2191,9 +2153,9 @@ dependencies = [ [[package]] name = "security-framework" -version = "2.4.2" +version = "2.3.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "525bc1abfda2e1998d152c45cf13e696f76d0a4972310b22fac1658b05df7c87" +checksum = "23a2ac85147a3a11d77ecf1bc7166ec0b92febfa4461c37944e180f319ece467" dependencies = [ "bitflags", "core-foundation", @@ -2226,9 +2188,9 @@ checksum = "9dad3f759919b92c3068c696c15c3d17238234498bbdcc80f2c469606f948ac8" [[package]] name = "serde" -version = "1.0.131" +version = "1.0.133" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4ad69dfbd3e45369132cc64e6748c2d65cdfb001a2b1c232d128b4ad60561c1" +checksum = "97565067517b60e2d1ea8b268e59ce036de907ac523ad83a0475da04e818989a" dependencies = [ "serde_derive", ] @@ -2247,9 +2209,9 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.131" +version = "1.0.133" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b710a83c4e0dff6a3d511946b95274ad9ca9e5d3ae497b63fda866ac955358d2" +checksum = "ed201699328568d8d08208fdd080e3ff594e6c422e438b6705905da01005d537" dependencies = [ "proc-macro2", "quote", @@ -2258,13 +2220,13 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.73" +version = "1.0.74" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bcbd0344bc6533bc7ec56df11d42fb70f1b912351c0825ccb7211b59d8af7cf5" +checksum = "ee2bb9cd061c5865d345bb02ca49fcef1391741b672b54a0bf7b679badec3142" dependencies = [ "itoa 1.0.1", "ryu", - "serde 1.0.131", + "serde 1.0.133", ] [[package]] @@ -2275,7 +2237,7 @@ checksum = "9ec5d77e2d4c73717816afac02670d5c4f534ea95ed430442cad02e7a6e32c97" dependencies = [ "dtoa", "itoa 0.4.8", - "serde 1.0.131", + "serde 1.0.133", "url", ] @@ -2288,7 +2250,7 @@ dependencies = [ "form_urlencoded", "itoa 0.4.8", "ryu", - "serde 1.0.131", + "serde 1.0.133", ] [[package]] @@ -2356,9 +2318,9 @@ checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" [[package]] name = "syn" -version = "1.0.82" +version = "1.0.85" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8daf5dd0bb60cbd4137b1b587d2fc0ae729bc07cf01cd70b36a1ed5ade3b9d59" +checksum = "a684ac3dcd8913827e18cd09a68384ee66c1de24157e3c556c9ab16d85695fb7" dependencies = [ "proc-macro2", "quote", @@ -2412,13 +2374,13 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.2.0" +version = "3.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dac1c663cfc93810f88aed9b8941d48cabf856a1b111c29a40439018d870eb22" +checksum = "5cdb1ef4eaeeaddc8fbd371e5017057064af0911902ef36b39801f67cc6d79e4" dependencies = [ "cfg-if 1.0.0", + "fastrand", "libc", - "rand 0.8.4", "redox_syscall", "remove_dir_all 0.5.3", "winapi 0.3.9", @@ -2456,7 +2418,7 @@ dependencies = [ "prusti", "prusti-launch", "rustwide", - "serde 1.0.131", + "serde 1.0.133", "toml", ] @@ -2546,18 +2508,17 @@ dependencies = [ [[package]] name = "tokio" -version = "1.14.0" +version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70e992e41e0d2fb9f755b37446f20900f64446ef54874f40a60c78f021ac6144" +checksum = "fbbf1c778ec206785635ce8ad57fe52b3009ae9e0c9f574a728f3049d3e55838" dependencies = [ - "autocfg", "bytes 1.1.0", "libc", "memchr", "mio 0.7.14", "num_cpus", "once_cell", - "pin-project-lite 0.2.7", + "pin-project-lite 0.2.8", "signal-hook-registry", "winapi 0.3.9", ] @@ -2569,8 +2530,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "50145484efff8818b5ccd256697f36863f587da82cf8b409c53adf1e840798e3" dependencies = [ "futures-core", - "pin-project-lite 0.2.7", - "tokio 1.14.0", + "pin-project-lite 0.2.8", + "tokio 1.15.0", ] [[package]] @@ -2591,7 +2552,7 @@ checksum = "6d9e878ad426ca286e4dcae09cbd4e1973a7f8987d97570e2469703dd7f5720c" dependencies = [ "futures-util", "log", - "pin-project 0.4.28", + "pin-project 0.4.29", "tokio 0.2.25", "tungstenite", ] @@ -2616,7 +2577,7 @@ version = "0.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a31142970826733df8241ef35dc040ef98c679ab14d7c3e54d827099b3acecaa" dependencies = [ - "serde 1.0.131", + "serde 1.0.133", ] [[package]] @@ -2633,7 +2594,7 @@ checksum = "375a639232caf30edfc78e8d89b2d4c375515393e7af7e16f01cd96917fb2105" dependencies = [ "cfg-if 1.0.0", "log", - "pin-project-lite 0.2.7", + "pin-project-lite 0.2.8", "tracing-core", ] @@ -2652,7 +2613,7 @@ version = "0.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "97d095ae15e245a057c8e8451bab9b3ee1e1f68e9ba2b4fbc18d0ac5237835f2" dependencies = [ - "pin-project 1.0.8", + "pin-project 1.0.10", "tracing", ] @@ -2664,13 +2625,13 @@ checksum = "59547bce71d9c38b83d9c0e92b6066c4253371f15005def0c30d9657f50c7642" [[package]] name = "trybuild" -version = "1.0.53" +version = "1.0.54" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9d664de8ea7e531ad4c0f5a834f20b8cb2b8e6dfe88d05796ee7887518ed67b9" +checksum = "f04343ff86b62ca40bd5dca986aadf4f10c152a9ebe9a869e456b60fa85afd3f" dependencies = [ "glob", - "lazy_static", - "serde 1.0.131", + "once_cell", + "serde 1.0.133", "serde_json", "termcolor", "toml", @@ -2706,9 +2667,9 @@ dependencies = [ [[package]] name = "typenum" -version = "1.14.0" +version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b63708a265f51345575b27fe43f9500ad611579e764c79edbc2037b1121959ec" +checksum = "dcf81ac59edc17cc8697ff311e8f5ef2d99fcbd9817b34cec66f90b6c3dfd987" [[package]] name = "unicase" @@ -2754,12 +2715,13 @@ checksum = "a156c684c91ea7d62626509bce3cb4e1d9ed5c4d978f7b4352658f96a4c26b4a" [[package]] name = "ureq" -version = "2.3.1" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c5c448dcb78ec38c7d59ec61f87f70a98ea19171e06c139357e012ee226fec90" +checksum = "9399fa2f927a3d327187cbd201480cee55bee6ac5d3c77dd27f0c6814cff16d5" dependencies = [ "base64 0.13.0", "chunked_transfer", + "flate2", "log", "once_cell", "rustls", @@ -2799,7 +2761,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bc5cf98d8186244414c848017f0e2676b3fcb46807f6668a97dfe67359a3c4b7" dependencies = [ "getrandom 0.2.3", - "serde 1.0.131", + "serde 1.0.133", ] [[package]] @@ -2816,9 +2778,9 @@ checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" [[package]] name = "version_check" -version = "0.9.3" +version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5fecdca9a5291cc2b8dcf7dc02453fee791a280f3743cb0905f8822ae463b3fe" +checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" [[package]] name = "viper" @@ -2831,7 +2793,7 @@ dependencies = [ "lazy_static", "log", "rustc-hash", - "serde 1.0.131", + "serde 1.0.133", "uuid", "viper-sys", ] @@ -2863,7 +2825,7 @@ dependencies = [ "quote", "regex", "rustc-hash", - "serde 1.0.131", + "serde 1.0.133", "syn", "thiserror", "uuid", @@ -2916,9 +2878,9 @@ dependencies = [ "mime", "mime_guess", "multipart", - "pin-project 0.4.28", + "pin-project 0.4.29", "scoped-tls", - "serde 1.0.131", + "serde 1.0.133", "serde_json", "serde_urlencoded 0.6.1", "tokio 0.2.25", @@ -2948,7 +2910,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "632f73e236b219150ea279196e54e610f5dbafa5d61786303d4da54f84e47fce" dependencies = [ "cfg-if 1.0.0", - "serde 1.0.131", + "serde 1.0.133", "serde_json", "wasm-bindgen-macro", ] @@ -3031,9 +2993,9 @@ dependencies = [ [[package]] name = "webpki-roots" -version = "0.22.1" +version = "0.22.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c475786c6f47219345717a043a37ec04cb4bc185e28853adcc4fa0a947eba630" +checksum = "552ceb903e957524388c4d3475725ff2c8b7960922063af6ce53c9a43da07449" dependencies = [ "webpki", ] diff --git a/analysis/src/domains/definitely_accessible/state.rs b/analysis/src/domains/definitely_accessible/state.rs index 2b401a96247..a6436fc7574 100644 --- a/analysis/src/domains/definitely_accessible/state.rs +++ b/analysis/src/domains/definitely_accessible/state.rs @@ -215,7 +215,7 @@ fn pretty_print_place<'tcx>( variant = Some(variant_index); } mir::ProjectionElem::Field(field, field_ty) => { - let field_name = describe_field_from_ty(prev_ty, field, variant)?; + let field_name = describe_field_from_ty(tcx, prev_ty, field, variant)?; pieces.push(format!(".{})", field_name)); prev_ty = field_ty; variant = None; @@ -233,14 +233,15 @@ fn pretty_print_place<'tcx>( } /// End-user visible description of the `field_index`nth field of `ty` -fn describe_field_from_ty( +fn describe_field_from_ty<'tcx>( + tcx: TyCtxt<'tcx>, ty: ty::Ty<'_>, field: mir::Field, variant_index: Option, ) -> Option { if ty.is_box() { // If the type is a box, the field is described from the boxed type - describe_field_from_ty(ty.boxed_ty(), field, variant_index) + describe_field_from_ty(tcx, ty.boxed_ty(), field, variant_index) } else { match *ty.kind() { ty::TyKind::Adt(def, _) => { @@ -250,14 +251,14 @@ fn describe_field_from_ty( } else { def.non_enum_variant() }; - Some(variant.fields[field.index()].ident.to_string()) + Some(variant.fields[field.index()].ident(tcx).to_string()) } ty::TyKind::Tuple(_) => Some(field.index().to_string()), ty::TyKind::Ref(_, ty, _) | ty::TyKind::RawPtr(ty::TypeAndMut { ty, .. }) => { - describe_field_from_ty(ty, field, variant_index) + describe_field_from_ty(tcx, ty, field, variant_index) } ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) => { - describe_field_from_ty(ty, field, variant_index) + describe_field_from_ty(tcx, ty, field, variant_index) } ty::TyKind::Closure(..) | ty::TyKind::Generator(..) => { // Supporting these cases is complex diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs index 1d19e3fc302..e6c6fa0a8a8 100644 --- a/prusti-interface/src/environment/mod.rs +++ b/prusti-interface/src/environment/mod.rs @@ -278,9 +278,9 @@ impl<'tcx> Environment<'tcx> { /// Get all relevant trait declarations for some type. pub fn get_traits_decls_for_type(&self, ty: &ty::Ty<'tcx>) -> HashSet { let mut res = HashSet::new(); - let traits = self.tcx().all_traits(()); - for trait_id in traits.iter() { - self.tcx().for_each_relevant_impl(*trait_id, ty, |impl_id| { + let traits = self.tcx().all_traits(); + for trait_id in traits { + self.tcx().for_each_relevant_impl(trait_id, ty, |impl_id| { if let Some(relevant_trait_id) = self.tcx().trait_id_of_impl(impl_id) { res.insert(relevant_trait_id); } diff --git a/prusti-specs/src/specifications/common.rs b/prusti-specs/src/specifications/common.rs index 1b5d82fc785..3a418567845 100644 --- a/prusti-specs/src/specifications/common.rs +++ b/prusti-specs/src/specifications/common.rs @@ -367,6 +367,7 @@ impl ProcedureSpecific /// /// In other words, any pre-/post-condition provided by `other` will overwrite any provided by /// `self`. + #[must_use] pub fn refine(&self, other: &Self) -> Self { let pres = if other.pres.is_empty() { self.pres.clone() diff --git a/prusti-specs/src/specifications/untyped.rs b/prusti-specs/src/specifications/untyped.rs index 1440b3b2e18..b60aa7bf486 100644 --- a/prusti-specs/src/specifications/untyped.rs +++ b/prusti-specs/src/specifications/untyped.rs @@ -235,17 +235,17 @@ impl AssignExpressionId for common::TriggerSet<(), syn::Expr> { spec_id: SpecificationId, id_generator: &mut ExpressionIdGenerator, ) -> TriggerSet { - TriggerSet { - 0: self.0 + common::TriggerSet( + self.0 .into_iter() - .map(|x| common::Trigger { - 0: x.0 + .map(|x| common::Trigger( + x.0 .into_iter() .map(|y| y.assign_id(spec_id, id_generator)) .collect() - }) + )) .collect() - } + ) } } diff --git a/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout b/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout index 8a568bdaa92..52499436935 100644 --- a/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout +++ b/prusti-tests/tests/cargo_verify/prusti_toml/output.stdout @@ -20,7 +20,7 @@ fn prusti_post_item_test1_[..](result: ()) { || -> bool { false }; } #[prusti::post_spec_id_ref = "[..]"] -pub fn test1() { } +pub fn test1() {} pub fn test2() { if !false { ::core::panicking::panic("assertion failed: false") }; } diff --git a/prusti-tests/tests/parse/ui/after_expiry.stdout b/prusti-tests/tests/parse/ui/after_expiry.stdout index b95451253b2..4fac74822e2 100644 --- a/prusti-tests/tests/parse/ui/after_expiry.stdout +++ b/prusti-tests/tests/parse/ui/after_expiry.stdout @@ -42,7 +42,7 @@ fn prusti_post_item_test1_$(NUM_UUID)(a: bool, } #[prusti::pledge_spec_id_ref = "$(NUM_UUID):$(NUM_UUID)"] -fn test1(a: bool) { } +fn test1(a: bool) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -69,7 +69,7 @@ fn prusti_post_item_test2_$(NUM_UUID)(a: bool, } #[prusti::pledge_spec_id_ref = "$(NUM_UUID):$(NUM_UUID)"] -fn test2(a: bool) { } +fn test2(a: bool) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -83,7 +83,7 @@ fn prusti_post_item_test3_$(NUM_UUID)(a: bool, || -> bool { a }; } #[prusti::pledge_spec_id_ref = ":$(NUM_UUID)"] -fn test3(a: bool) { } +fn test3(a: bool) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -97,7 +97,7 @@ fn prusti_post_item_test4_$(NUM_UUID)(a: bool, || -> bool { a }; } #[prusti::pledge_spec_id_ref = ":$(NUM_UUID)"] -fn test4(a: bool) { } +fn test4(a: bool) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/parse/ui/and.stdout b/prusti-tests/tests/parse/ui/and.stdout index b4fd5f01291..62e6bba9538 100644 --- a/prusti-tests/tests/parse/ui/and.stdout +++ b/prusti-tests/tests/parse/ui/and.stdout @@ -32,7 +32,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -53,7 +53,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -74,7 +74,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -95,7 +95,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -120,7 +120,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: And([Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:6 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:7 ~ and[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#1}) }) }]) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: And([Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:10 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:11 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#1}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:12 ~ and[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#2}) }) }]) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/parse/ui/composite.stdout b/prusti-tests/tests/parse/ui/composite.stdout index 0a220b273c6..53bb9c456c9 100644 --- a/prusti-tests/tests/parse/ui/composite.stdout +++ b/prusti-tests/tests/parse/ui/composite.stdout @@ -56,7 +56,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -85,7 +85,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -106,7 +106,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -131,7 +131,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -160,7 +160,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() { || -> bool { true || true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -193,7 +193,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test6() { } +fn test6() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -226,7 +226,7 @@ fn prusti_pre_item_test7_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test7() { } +fn test7() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -243,7 +243,7 @@ fn prusti_pre_item_test8_$(NUM_UUID)() { || -> bool { true || true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test8() { } +fn test8() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -260,7 +260,7 @@ fn prusti_pre_item_test9_$(NUM_UUID)() { || -> bool { true || (true && (true || true)) }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test9() { } +fn test9() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -283,7 +283,7 @@ fn prusti_pre_item_test10_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test10() { } +fn test10() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -302,7 +302,7 @@ fn prusti_pre_item_test12_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test12() { } +fn test12() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -329,7 +329,7 @@ fn prusti_pre_item_test13_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test13() { } +fn test13() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -352,7 +352,7 @@ fn prusti_pre_item_test14_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test14() { } +fn test14() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -375,7 +375,7 @@ fn prusti_pre_item_test15_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test15() { } +fn test15() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -408,7 +408,7 @@ fn prusti_pre_item_test16_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test16() { } +fn test16() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -431,7 +431,7 @@ fn prusti_pre_item_test17_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test17() { } +fn test17() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -450,7 +450,7 @@ fn prusti_pre_item_test19_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test19() { } +fn test19() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -477,7 +477,7 @@ fn prusti_pre_item_test20_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test20() { } +fn test20() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -500,7 +500,7 @@ fn prusti_pre_item_test21_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test21() { } +fn test21() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -523,7 +523,7 @@ fn prusti_pre_item_test22_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test22() { } +fn test22() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -556,7 +556,7 @@ fn prusti_pre_item_test23_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test23() { } +fn test23() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:99 ~ composite[$(CRATE_ID)]::prusti_pre_item_test19_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:67 ~ composite[$(CRATE_ID)]::prusti_pre_item_test12_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/parse/ui/exists.stdout b/prusti-tests/tests/parse/ui/exists.stdout index d01558318c2..6e03aeaf8d6 100644 --- a/prusti-tests/tests/parse/ui/exists.stdout +++ b/prusti-tests/tests/parse/ui/exists.stdout @@ -35,7 +35,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -54,7 +54,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -77,7 +77,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -104,7 +104,7 @@ fn prusti_pre_item_test8_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test8() { } +fn test8() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -135,7 +135,7 @@ fn prusti_pre_item_test9_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test9() { } +fn test9() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -182,7 +182,7 @@ fn prusti_pre_item_test10_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test10() { } +fn test10() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:7 ~ exists[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32), (_3, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:11 ~ exists[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/parse/ui/expression.stdout b/prusti-tests/tests/parse/ui/expression.stdout index 21b2ccf2c1e..1a710113bef 100644 --- a/prusti-tests/tests/parse/ui/expression.stdout +++ b/prusti-tests/tests/parse/ui/expression.stdout @@ -29,7 +29,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { || -> bool { 1 != 2 }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -42,7 +42,7 @@ fn prusti_post_item_test2_$(NUM_UUID)(result: ()) { || -> bool { 1 == 1 || 1 == 2 }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} fn main() {} Procedure(ProcedureSpecification { pres: [], posts: [Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:10 ~ expression[$(CRATE_ID)]::prusti_post_item_test2_$(NUM_UUID)::{closure#0}) }) }], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: And([Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:6 ~ expression[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:7 ~ expression[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#1}) }) }]) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/parse/ui/forall.stdout b/prusti-tests/tests/parse/ui/forall.stdout index 66fddb0ba06..52dc1a4cfe3 100644 --- a/prusti-tests/tests/parse/ui/forall.stdout +++ b/prusti-tests/tests/parse/ui/forall.stdout @@ -35,7 +35,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -54,7 +54,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -77,7 +77,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -104,7 +104,7 @@ fn prusti_pre_item_test8_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test8() { } +fn test8() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -135,7 +135,7 @@ fn prusti_pre_item_test9_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test9() { } +fn test9() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -182,7 +182,7 @@ fn prusti_pre_item_test10_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test10() { } +fn test10() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:7 ~ forall[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32), (_3, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:11 ~ forall[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/parse/ui/implies.stdout b/prusti-tests/tests/parse/ui/implies.stdout index 83b27c45f05..01bee3077bc 100644 --- a/prusti-tests/tests/parse/ui/implies.stdout +++ b/prusti-tests/tests/parse/ui/implies.stdout @@ -32,7 +32,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -53,7 +53,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -74,7 +74,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -95,7 +95,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -120,7 +120,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: Implies(Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:6 ~ implies[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:7 ~ implies[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#1}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: Implies(Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:10 ~ implies[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}) }) }, Assertion { kind: Implies(Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:11 ~ implies[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#1}) }) }, Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:12 ~ implies[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#2}) }) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/parse/ui/predicates-visibility.stdout b/prusti-tests/tests/parse/ui/predicates-visibility.stdout index 7e3082e1d06..3a45fade31d 100644 --- a/prusti-tests/tests/parse/ui/predicates-visibility.stdout +++ b/prusti-tests/tests/parse/ui/predicates-visibility.stdout @@ -67,7 +67,7 @@ fn prusti_pre_item_test_pub_pred_$(NUM_UUID)() { || -> bool { foo::pred1(true) }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test_pub_pred() { } +fn test_pub_pred() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:14 ~ predicates_visibility[$(CRATE_ID)]::prusti_pre_item_test_pub_pred_$(NUM_UUID)::{closure#0}) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [], posts: [], pledges: [], predicate_body: Some(Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, bool)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:11 ~ predicates_visibility[$(CRATE_ID)]::foo::prusti_pred_item_pred1_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }), pure: true, trusted: true }) diff --git a/prusti-tests/tests/parse/ui/predicates.stdout b/prusti-tests/tests/parse/ui/predicates.stdout index 5d6e2b5ed11..7caf10f1537 100644 --- a/prusti-tests/tests/parse/ui/predicates.stdout +++ b/prusti-tests/tests/parse/ui/predicates.stdout @@ -67,7 +67,7 @@ fn prusti_pre_item_use_pred1_$(NUM_UUID)() { || -> bool { pred1(true) }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn use_pred1() { } +fn use_pred1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -116,7 +116,7 @@ fn prusti_pre_item_use_pred2_$(NUM_UUID)() { || -> bool { pred2(true) }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn use_pred2() { } +fn use_pred2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/parse/ui/spec_entailment.stdout b/prusti-tests/tests/parse/ui/spec_entailment.stdout index 3cb18a2a1ba..d6e63e2cdc2 100644 --- a/prusti-tests/tests/parse/ui/spec_entailment.stdout +++ b/prusti-tests/tests/parse/ui/spec_entailment.stdout @@ -50,7 +50,7 @@ fn prusti_pre_item_test1_$(NUM_UUID) i32>(f: F) { } +fn test1 i32>(f: F) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -78,7 +78,7 @@ fn prusti_pre_item_test2_$(NUM_UUID) i32>(g: F) { } +fn test2 i32>(g: F) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -106,7 +106,7 @@ fn prusti_pre_item_test3_$(NUM_UUID) i32>(f: F) { } +fn test3 i32>(f: F) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -140,7 +140,7 @@ fn prusti_pre_item_test4_$(NUM_UUID) i32>(f: F) { } +fn test4 i32>(f: F) {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: SpecEntailment { closure: Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:16 ~ spec_entailment[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}) }, arg_binders: SpecEntailmentVars { spec_id: SpecificationId($(UUID)), pre_id: ExpressionId(102), post_id: ExpressionId(103), args: [(_2, i32)], result: (_3, i32) }, pres: [Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(104), expr: DefId(0:18 ~ spec_entailment[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#1}::{closure#0}) }) }], posts: [] } }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: SpecEntailment { closure: Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), expr: DefId(0:24 ~ spec_entailment[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID)::{closure#0}) }, arg_binders: SpecEntailmentVars { spec_id: SpecificationId($(UUID)), pre_id: ExpressionId(102), post_id: ExpressionId(103), args: [(_2, i32)], result: (_3, i32) }, pres: [], posts: [Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(104), expr: DefId(0:27 ~ spec_entailment[$(CRATE_ID)]::prusti_pre_item_test3_$(NUM_UUID)::{closure#2}::{closure#0}) }) }] } }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/parse/ui/trait-bounds.stdout b/prusti-tests/tests/parse/ui/trait-bounds.stdout index 0863d60b2cb..9365560704c 100644 --- a/prusti-tests/tests/parse/ui/trait-bounds.stdout +++ b/prusti-tests/tests/parse/ui/trait-bounds.stdout @@ -16,7 +16,7 @@ extern crate std; extern crate prusti_contracts; use prusti_contracts::*; struct Foo<'a, T: PartialEq, const L : usize>(&'a [T; L]); -impl <'a, T: PartialEq, const L : usize> Foo<'a, T, L> { +impl<'a, T: PartialEq, const L : usize> Foo<'a, T, L> { pub fn bar(self) -> &'a [T; L] { self.0 } } #[allow(non_camel_case_types)] @@ -24,7 +24,7 @@ struct PrustiStructFoo_$(NUM_UUID)<'a, T: PartialEq, const L : usize>(&'a ::core::marker::PhantomData<()>, ::core::marker::PhantomData); -impl <'a, T: PartialEq, const L : usize> +impl<'a, T: PartialEq, const L : usize> PrustiStructFoo_$(NUM_UUID)<'a, T, L> { #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] diff --git a/prusti-tests/tests/parse/ui/traits.stdout b/prusti-tests/tests/parse/ui/traits.stdout index ed06f9babf3..c64e243cb80 100644 --- a/prusti-tests/tests/parse/ui/traits.stdout +++ b/prusti-tests/tests/parse/ui/traits.stdout @@ -44,7 +44,7 @@ trait Test1 { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] - fn test1() { } + fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -57,7 +57,7 @@ trait Test1 { || -> bool { true }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] - fn test2() { } + fn test2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -110,7 +110,7 @@ trait Test2 { } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] - fn test1() { } + fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -150,7 +150,7 @@ trait Test3 { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] - fn test1(&self) { } + fn test1(&self) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -164,7 +164,7 @@ trait Test3 { || -> bool { true }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] - fn test2(&self) { } + fn test2(&self) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -219,7 +219,7 @@ trait Test4 { } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] - fn test1(&self) { } + fn test1(&self) {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/parse/ui/true.stdout b/prusti-tests/tests/parse/ui/true.stdout index 505ecaddcd9..8e603cf799b 100644 --- a/prusti-tests/tests/parse/ui/true.stdout +++ b/prusti-tests/tests/parse/ui/true.stdout @@ -27,7 +27,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -40,7 +40,7 @@ fn prusti_post_item_test2_$(NUM_UUID)(result: ()) { || -> bool { true }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} fn test3() { for _ in 0..2 { diff --git a/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout b/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout index 473a0b80575..df76a82559d 100644 --- a/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout +++ b/prusti-tests/tests/typecheck/ui/forall_encode_typeck.stdout @@ -43,7 +43,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -74,7 +74,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32), (_3, u32)] }, TriggerSet([Trigger([Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:8 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}::{closure#1}) }, Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:9 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}::{closure#2}) }]), Trigger([Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(104), expr: DefId(0:10 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}::{closure#3}) }])]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(105), expr: DefId(0:7 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32), (_3, u32)] }, TriggerSet([Trigger([Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:15 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}::{closure#1}) }, Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:16 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}::{closure#2}) }]), Trigger([Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(104), expr: DefId(0:17 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}::{closure#3}) }])]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(105), expr: DefId(0:14 ~ forall_encode_typeck[$(CRATE_ID)]::prusti_pre_item_test2_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/typecheck/ui/forall_triggers.stdout b/prusti-tests/tests/typecheck/ui/forall_triggers.stdout index 1baa897834c..e06b1ec9dcd 100644 --- a/prusti-tests/tests/typecheck/ui/forall_triggers.stdout +++ b/prusti-tests/tests/typecheck/ui/forall_triggers.stdout @@ -41,7 +41,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -71,7 +71,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -106,7 +106,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -141,7 +141,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -164,7 +164,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -194,7 +194,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test6() { } +fn test6() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -229,7 +229,7 @@ fn prusti_pre_item_test7_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test7() { } +fn test7() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -264,7 +264,7 @@ fn prusti_pre_item_test8_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test8() { } +fn test8() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([Trigger([Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:8 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}::{closure#1}) }])]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:7 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([Trigger([Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:33 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID)::{closure#0}::{closure#1}) }])]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:32 ~ forall_triggers[$(CRATE_ID)]::prusti_pre_item_test5_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/typecheck/ui/nested_forall.stdout b/prusti-tests/tests/typecheck/ui/nested_forall.stdout index db36819aa15..67737d10ac8 100644 --- a/prusti-tests/tests/typecheck/ui/nested_forall.stdout +++ b/prusti-tests/tests/typecheck/ui/nested_forall.stdout @@ -43,7 +43,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -74,7 +74,7 @@ fn prusti_pre_item_test2_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -112,7 +112,7 @@ fn prusti_pre_item_test3_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -138,7 +138,7 @@ fn prusti_pre_item_test4_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -169,7 +169,7 @@ fn prusti_pre_item_test5_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -207,7 +207,7 @@ fn prusti_pre_item_test6_$(NUM_UUID)() { }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test6() { } +fn test6() {} fn main() {} Procedure(ProcedureSpecification { pres: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:8 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test1_$(NUM_UUID)::{closure#0}::{closure#0}::{closure#0}) }) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) Procedure(ProcedureSpecification { pres: [Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Exists(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(103), expr: DefId(0:26 ~ nested_forall[$(CRATE_ID)]::prusti_pre_item_test4_$(NUM_UUID)::{closure#0}::{closure#0}::{closure#0}) }) }) }) }], posts: [], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/verify/ui/collect.stdout b/prusti-tests/tests/verify/ui/collect.stdout index f91cd8264ff..54f81f211b6 100644 --- a/prusti-tests/tests/verify/ui/collect.stdout +++ b/prusti-tests/tests/verify/ui/collect.stdout @@ -27,7 +27,7 @@ fn prusti_pre_item_test1_$(NUM_UUID)() { || -> bool { true }; } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -40,7 +40,7 @@ fn prusti_post_item_test2_$(NUM_UUID)(result: ()) { || -> bool { true }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} fn test3() { let mut curr = 0; while curr < 2 { diff --git a/prusti-tests/tests/verify/ui/false.stdout b/prusti-tests/tests/verify/ui/false.stdout index 95f415a6a4c..142746532a8 100644 --- a/prusti-tests/tests/verify/ui/false.stdout +++ b/prusti-tests/tests/verify/ui/false.stdout @@ -25,7 +25,7 @@ fn prusti_post_item_test1_$(NUM_UUID)(result: ()) { || -> bool { false }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} fn test2() { if !false { ::core::panicking::panic("assertion failed: false") }; } diff --git a/prusti-tests/tests/verify/ui/forall_verify.stdout b/prusti-tests/tests/verify/ui/forall_verify.stdout index b06a8bf9d2e..61a12a8e91a 100644 --- a/prusti-tests/tests/verify/ui/forall_verify.stdout +++ b/prusti-tests/tests/verify/ui/forall_verify.stdout @@ -42,7 +42,7 @@ fn prusti_post_item_test1_$(NUM_UUID)(result: ()) { }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test1() { } +fn test1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -61,7 +61,7 @@ fn prusti_post_item_test2_$(NUM_UUID)(result: ()) { }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test2() { } +fn test2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -80,7 +80,7 @@ fn prusti_post_item_test3_$(NUM_UUID)(result: ()) { }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test3() { } +fn test3() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -99,7 +99,7 @@ fn prusti_post_item_test4_$(NUM_UUID)(result: ()) { }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test4() { } +fn test4() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -130,7 +130,7 @@ fn prusti_post_item_test5_$(NUM_UUID)(result: ()) { } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test5() { } +fn test5() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -149,7 +149,7 @@ fn prusti_post_item_test6_$(NUM_UUID)(result: ()) { }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test6() { } +fn test6() {} fn main() {} Procedure(ProcedureSpecification { pres: [], posts: [], pledges: [], predicate_body: None, pure: true, trusted: false }) Procedure(ProcedureSpecification { pres: [], posts: [Assertion { kind: ForAll(QuantifierVars { spec_id: SpecificationId($(UUID)), id: ExpressionId(101), vars: [(_2, i32)] }, TriggerSet([]), Assertion { kind: Expr(Expression { spec_id: SpecificationId($(UUID)), id: ExpressionId(102), expr: DefId(0:8 ~ forall_verify[$(CRATE_ID)]::prusti_post_item_test1_$(NUM_UUID)::{closure#0}::{closure#0}) }) }) }], pledges: [], predicate_body: None, pure: false, trusted: false }) diff --git a/prusti-tests/tests/verify/ui/predicate.stdout b/prusti-tests/tests/verify/ui/predicate.stdout index ae96c7c5fe2..617f3a77b5f 100644 --- a/prusti-tests/tests/verify/ui/predicate.stdout +++ b/prusti-tests/tests/verify/ui/predicate.stdout @@ -198,7 +198,7 @@ fn prusti_pre_item_test_identity_1_$(NUM_UUID)() { } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test_identity_1() { } +fn test_identity_1() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] @@ -223,7 +223,7 @@ fn prusti_pre_item_test_identity_2_$(NUM_UUID)() { } #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] #[prusti::pre_spec_id_ref = "$(NUM_UUID)"] -fn test_identity_2() { } +fn test_identity_2() {} #[allow(unused_must_use, unused_variables, dead_code)] #[prusti::spec_only] #[prusti::spec_id = "$(NUM_UUID)"] diff --git a/prusti-tests/tests/verify/ui/pure.stdout b/prusti-tests/tests/verify/ui/pure.stdout index a6078107261..282cadcfd8d 100644 --- a/prusti-tests/tests/verify/ui/pure.stdout +++ b/prusti-tests/tests/verify/ui/pure.stdout @@ -46,7 +46,7 @@ fn prusti_post_item_test_identity2_$(NUM_UUID)(result: || -> bool { 6 == identity(6) }; } #[prusti::post_spec_id_ref = "$(NUM_UUID)"] -fn test_identity2() { } +fn test_identity2() {} #[prusti::pure] fn max(a: i32, b: i32) -> i32 { if a > b { a } else { b } } fn test_max1() { diff --git a/prusti-viper/src/encoder/counterexample_translation.rs b/prusti-viper/src/encoder/counterexample_translation.rs index dfb3eddb97b..cde1e42d17e 100644 --- a/prusti-viper/src/encoder/counterexample_translation.rs +++ b/prusti-viper/src/encoder/counterexample_translation.rs @@ -262,7 +262,7 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> { } (ty::TyKind::Adt(adt_def, subst), _) if adt_def.is_struct() => { let variant = adt_def.variants.iter().next().unwrap(); - let struct_name = variant.ident.name.to_ident_string(); + let struct_name = variant.ident(self.tcx).name.to_ident_string(); let field_entries = self.translate_vardef( variant, sil_entry, @@ -302,7 +302,7 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> { let discriminant = x.parse::().unwrap(); variant = adt_def.variants.iter().find(|x| get_discriminant_of_vardef(x) == Some(discriminant)); if let Some(v) = variant { - variant_name = v.ident.name.to_ident_string(); + variant_name = v.ident(self.tcx).name.to_ident_string(); } } @@ -345,7 +345,7 @@ impl<'ce, 'tcx> CounterexampleTranslator<'ce, 'tcx> { ) -> Vec<(String, Entry)> { let mut field_entries = vec![]; for f in &variant.fields { - let field_name = f.ident.name.to_ident_string(); + let field_name = f.ident(self.tcx).name.to_ident_string(); let typ = f.ty(self.tcx, subst); // extract recursively diff --git a/prusti-viper/src/encoder/mir/procedures/encoder.rs b/prusti-viper/src/encoder/mir/procedures/encoder.rs index 885848bdf24..2e4b681ae40 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder.rs @@ -196,7 +196,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { ) -> SpannedEncodingResult<()> { let span = self.encoder.get_span_of_location(self.mir, location); match aggregate_kind { - mir::AggregateKind::Adt(adt_def, variant_index, substs, _, active_field_index) => { + mir::AggregateKind::Adt(adt_did, variant_index, substs, _, active_field_index) => { + let adt_def = self.encoder.env().tcx().adt_def(*adt_did); assert!( active_field_index.is_none(), "field index should be set only for unions" diff --git a/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs b/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs index a03196002f5..e403cf03d5f 100644 --- a/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs +++ b/prusti-viper/src/encoder/mir/pure/interpreter/mod.rs @@ -126,13 +126,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> ExpressionBackwardInterpreter<'p, 'v, 'tcx> { let rhs = vir_high::Expression::constructor_no_pos(ty, arguments); state.substitute_value(lhs, rhs); } - mir::AggregateKind::Adt(adt_def, variant_index, _, _, _) => { + mir::AggregateKind::Adt(adt_did, variant_index, _, _, _) => { + let tcx = self.encoder.env().tcx(); + let adt_def = tcx.adt_def(*adt_did); let ty_with_variant = if adt_def.variants.len() > 1 { // FIXME: Shouls use adt_def.is_enum() as a check. // FIXME: Most likely need to substitute the discriminant here. let variant_def = &adt_def.variants[*variant_index]; - let variant_name: &str = &variant_def.ident.as_str(); - ty.variant(variant_name.to_string().into()) + let variant_name = variant_def.ident(tcx).to_string(); + ty.variant(variant_name.into()) } else { ty }; diff --git a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs index 53e0d4d53f1..b0ff3e64c75 100644 --- a/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs +++ b/prusti-viper/src/encoder/mir/pure/pure_functions/interpreter.rs @@ -89,8 +89,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> PureFunctionBackwardInterpreter<'p, 'v, 'tcx> { .encode_projection(place.local, &place.projection[..]) .with_span(span)?; let variant_field = if let ty::TyKind::Adt(adt_def, _subst) = place_ty.kind() { - let variant_name = &adt_def.variants[variant_idx].ident.as_str(); - self.encoder.encode_enum_variant_field(variant_name) + let tcx = self.encoder.env().tcx(); + let variant_name = adt_def.variants[variant_idx].ident(tcx).to_string(); + self.encoder.encode_enum_variant_field(&variant_name) } else { unreachable!() }; @@ -846,7 +847,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> state.substitute_value(&encoded_lhs, snapshot); } - &mir::AggregateKind::Adt(adt_def, variant_index, subst, _, _) => { + &mir::AggregateKind::Adt(adt_did, variant_index, subst, _, _) => { + let tcx = self.encoder.env().tcx(); + let adt_def = tcx.adt_def(adt_did); let num_variants = adt_def.variants.len(); let variant_def = &adt_def.variants[variant_index]; let mut encoded_lhs_variant = encoded_lhs.clone(); @@ -857,17 +860,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> BackwardMirInterpreter<'tcx> variant_index.index().into(), ); encoded_lhs_variant = - encoded_lhs_variant.variant(&variant_def.ident.as_str()); + encoded_lhs_variant.variant(&variant_def.ident(tcx).as_str()); } let mut field_exprs = vec![]; for (field_index, field) in variant_def.fields.iter().enumerate() { let operand = &operands[field_index]; - let field_name = &field.ident.as_str(); - let tcx = self.encoder.env().tcx(); + let field_name = field.ident(tcx).to_string(); let field_ty = field.ty(tcx, subst); let encoded_field = self.encoder - .encode_struct_field(field_name, field_ty) - .with_span(span)?; + .encode_struct_field(&field_name, field_ty) + .with_span(span)?; let field_place = encoded_lhs_variant.clone().field(encoded_field); diff --git a/prusti-viper/src/encoder/mir/types/encoder.rs b/prusti-viper/src/encoder/mir/types/encoder.rs index d9f8018c024..c20e61b3409 100644 --- a/prusti-viper/src/encoder/mir/types/encoder.rs +++ b/prusti-viper/src/encoder/mir/types/encoder.rs @@ -732,7 +732,7 @@ fn encode_variant<'v, 'tcx: 'v>( let tcx = encoder.env().tcx(); let mut fields = Vec::new(); for field in &variant.fields { - let field_name = crate::encoder::encoder::encode_field_name(&field.ident.as_str()); + let field_name = crate::encoder::encoder::encode_field_name(&field.ident(tcx).as_str()); let field_ty = field.ty(tcx, substs); let field = vir::FieldDecl::new(field_name, encoder.encode_type_high(field_ty)?); fields.push(field); @@ -792,9 +792,8 @@ pub(super) fn encode_adt_def<'v, 'tcx>( .collect(); let mut variants = Vec::new(); for variant in &adt_def.variants { - let name = &variant.ident.as_str(); - let encoded_variant = - encode_variant(encoder, (*name).to_string(), substs, variant)?; + let name = variant.ident(tcx).to_string(); + let encoded_variant = encode_variant(encoder, name, substs, variant)?; variants.push(encoded_variant); } vir::TypeDecl::enum_(name, discriminant_bounds, discriminant_values, variants) diff --git a/prusti-viper/src/encoder/mir/types/interface.rs b/prusti-viper/src/encoder/mir/types/interface.rs index ea4d689e940..fd6d40944e0 100644 --- a/prusti-viper/src/encoder/mir/types/interface.rs +++ b/prusti-viper/src/encoder/mir/types/interface.rs @@ -178,7 +178,7 @@ impl<'v, 'tcx: 'v> MirTypeEncoderInterface<'tcx> for super::super::super::Encode ) -> EncodingResult { if let ty::TyKind::Adt(adt_def, _) = ty.kind() { let variant = &adt_def.variants[variant_index]; - let name = variant.ident.to_string(); + let name = variant.ident(self.env().tcx()).to_string(); Ok(name.into()) } else { Err(EncodingError::internal(format!("{:?} is not an enum", ty))) diff --git a/prusti-viper/src/encoder/mir_encoder/mod.rs b/prusti-viper/src/encoder/mir_encoder/mod.rs index 761dfbb5bbd..c7c04ff7d3c 100644 --- a/prusti-viper/src/encoder/mir_encoder/mod.rs +++ b/prusti-viper/src/encoder/mir_encoder/mod.rs @@ -132,7 +132,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> { let tcx = self.encoder().env().tcx(); let variant_def = &adt_def.variants[variant_index.into()]; let encoded_variant = if num_variants != 1 { - encoded_base.variant(&variant_def.ident.as_str()) + encoded_base.variant(&variant_def.ident(tcx).as_str()) } else { encoded_base }; @@ -146,7 +146,7 @@ pub trait PlaceEncoder<'v, 'tcx: 'v> { let encoded_field = self .encoder() .encode_struct_field( - &field.ident.as_str(), + &field.ident(tcx).as_str(), field_ty )?; let encoded_projection = encoded_variant.field(encoded_field); @@ -829,7 +829,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> MirEncoder<'p, 'v, 'tcx> { .collect(); match ¯o_names_str[..] { ["core::panic::panic_2015", "core::macros::panic", "std::unimplemented"] => PanicCause::Unimplemented, + ["std::unimplemented", ..] => PanicCause::Unimplemented, ["core::panic::panic_2015", "core::macros::panic", "std::unreachable"] => PanicCause::Unreachable, + ["std::unreachable", ..] => PanicCause::Unreachable, ["std::assert", "std::debug_assert", ..] => PanicCause::DebugAssert, ["std::assert", ..] => PanicCause::Assert, ["std::panic::panic_2015", "std::panic", "std::debug_assert"] => PanicCause::DebugAssert, diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index 455256982d5..22bf96eb38e 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -1069,8 +1069,9 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { .encode_projection(place.local, &place.projection, ArrayAccessKind::Shared, location)?; downcast_stmts.extend(pre_stmts); let variant_field = if let ty::TyKind::Adt(adt_def, _) = place_ty.kind() { - let variant_name = &adt_def.variants[variant_idx].ident.as_str(); - self.encoder.encode_enum_variant_field(variant_name) + let tcx = self.encoder.env().tcx(); + let variant_name = adt_def.variants[variant_idx].ident(tcx).to_string(); + self.encoder.encode_enum_variant_field(&variant_name) } else { unreachable!() }; @@ -5579,7 +5580,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } /// Assignment with a nullary op on the RHS. - /// Nullary types currently are creating boxes and sizeof. + /// Nullary types currently are sizeof and alignof. /// [lhs] = [op] [op_ty] fn encode_assign_nullary_op( &mut self, @@ -5595,12 +5596,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { op_ty ); match op { - mir::NullOp::Box => self.encode_assign_box( - op_ty, - encoded_lhs, - ty, - location, - ), mir::NullOp::SizeOf => { // TODO: ParamEnv::empty() should probably be tyctxt.param_env(def_id_of_method) let bytes = self.encoder.env().tcx() @@ -6280,17 +6275,24 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } } - mir::AggregateKind::Adt(adt_def, variant_index, subst, _, _) if !adt_def.is_union() => { + mir::AggregateKind::Adt(adt_did, variant_index, subst, _, _) => { + let tcx = self.encoder.env().tcx(); + let adt_def = tcx.adt_def(adt_did); + if adt_def.is_union() { + return Err(SpannedEncodingError::unsupported( + "unions are not supported", + span + )); + } let num_variants = adt_def.variants.len(); let variant_def = &adt_def.variants[variant_index]; let mut dst_base = dst.clone(); if num_variants != 1 { // An enum. - let tcx = self.encoder.env().tcx(); // Handle *signed* discriminats let discr_value: vir::Expr = if let SignedInt(ity) = adt_def.repr.discr_type() { let bit_size = - Integer::from_attr(&self.encoder.env().tcx(), SignedInt(ity)) + Integer::from_attr(&tcx, SignedInt(ity)) .size() .bits(); let shift = 128 - bit_size; @@ -6313,8 +6315,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { expr: vir::Expr::eq_cmp(discriminant, discr_value), })); - let variant_name = &variant_def.ident.as_str(); - let new_dst_base = dst_base.variant(variant_name); + let variant_name = variant_def.ident(tcx).to_string(); + let new_dst_base = dst_base.variant(&variant_name); let variant_field = if let vir::Expr::Variant( vir::Variant {variant_index: ref field, ..}) = new_dst_base { field.clone() } else { @@ -6332,11 +6334,10 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } for (field_index, field) in variant_def.fields.iter().enumerate() { let operand = &operands[field_index]; - let field_name = &field.ident.as_str(); - let tcx = self.encoder.env().tcx(); + let field_name = field.ident(tcx).to_string(); let field_ty = field.ty(tcx, subst); let encoded_field = self.encoder - .encode_struct_field(field_name, field_ty) + .encode_struct_field(&field_name, field_ty) .with_span(span)?; stmts.extend(self.encode_assign_operand( &dst_base.clone().field(encoded_field), @@ -6346,14 +6347,6 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { } } - mir::AggregateKind::Adt(..) => { - // It is a union - return Err(SpannedEncodingError::unsupported( - "unions are not supported", - span - )); - } - mir::AggregateKind::Closure(def_id, _substs) => { debug_assert!(!self.encoder.is_spec_closure(def_id), "spec closure: {:?}", def_id); // TODO: assign to closure; this case should only handle assign diff --git a/prusti-viper/src/encoder/snapshot/encoder.rs b/prusti-viper/src/encoder/snapshot/encoder.rs index 696943648d1..1ccc890473b 100644 --- a/prusti-viper/src/encoder/snapshot/encoder.rs +++ b/prusti-viper/src/encoder/snapshot/encoder.rs @@ -726,12 +726,12 @@ impl SnapshotEncoder { // or adt_def.variants[0].fields ? let field_ty = field.ty(tcx, subst); fields.push(SnapshotField { - name: encode_field_name(&field.ident.to_string()), + name: encode_field_name(&field.ident(tcx).to_string()), access: self.snap_app( encoder, Expr::field( arg_expr.clone(), - encoder.encode_struct_field(&field.ident.to_string(), field_ty)?, + encoder.encode_struct_field(&field.ident(tcx).to_string(), field_ty)?, ), tymap, )?, @@ -774,13 +774,13 @@ impl SnapshotEncoder { for field in &variant.fields { let field_ty = field.ty(tcx, subst); fields.push(SnapshotField { - name: encode_field_name(&field.ident.to_string()), + name: encode_field_name(&field.ident(tcx).to_string()), access: self.snap_app( encoder, Expr::field( field_base.clone(), encoder - .encode_struct_field(&field.ident.to_string(), field_ty)?, + .encode_struct_field(&field.ident(tcx).to_string(), field_ty)?, ), tymap, )?, @@ -846,7 +846,7 @@ impl SnapshotEncoder { ); let array_collect_func_app = - array_collect_func.apply(vec![arg_expr.clone(), 0.into()]); + array_collect_func.apply(vec![arg_expr.clone(), 0usize.into()]); let snap_body = cons.apply(vec![array_collect_func_app]); diff --git a/rust-toolchain b/rust-toolchain index 0a3d06de7e4..fd1034a435d 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2021-12-15" +channel = "nightly-2022-01-13" components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt" ] profile = "minimal"