diff --git a/Cargo.lock b/Cargo.lock index 14328cf7d86..810ead6a36b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -30,9 +30,9 @@ dependencies = [ [[package]] name = "aho-corasick" -version = "1.0.5" +version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c378d78423fdad8089616f827526ee33c19f2fddbd5de1629152c9593ba4783" +checksum = "0f2135563fb5c609d2b2b87c1e8ce7bc41b0b45430fa9661f457981503dd5bf0" dependencies = [ "memchr", ] @@ -103,9 +103,9 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "15c4c2c83f81532e5845a733998b6971faca23490340a418e9b72a3ec9de12ea" +checksum = "b84bf0a05bbb2a83e5eb6fa36bb6e87baa08193c35ff52bbf6b38d8af2890e46" [[package]] name = "anstyle-parse" @@ -280,7 +280,7 @@ checksum = "bc00ceb34980c03614e35a3a4e218276a0a824e911d07651cd0d858a51e8c0f0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -339,9 +339,9 @@ checksum = "9e1b586273c5702936fe7b7d6896644d8be71e6314cfe09d3167c95f712589e8" [[package]] name = "base64" -version = "0.21.3" +version = "0.21.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "414dcefbc63d77c526a76b3afcf6fbb9b5e2791c19c3aa2297733208750c6e53" +checksum = "9ba43ea6f343b788c8764558649e08df62f86c6ef251fdaeb1ffd010a9ae50a2" [[package]] name = "base64ct" @@ -413,9 +413,9 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.13.0" +version = "3.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a3e2c3daef883ecc1b5d58c15adae93470a91d425f3532ba1695849656af3fc1" +checksum = "7f30e7476521f6f8af1a1c4c0b8cc94f0bee37d91763d0ca2665f299b6cd8aec" [[package]] name = "byteorder" @@ -425,9 +425,9 @@ checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610" [[package]] name = "bytes" -version = "1.4.0" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89b2fd2a0dcf38d7971e2194b6b6eebab45ae01067456a7fd93d5547a61b70be" +checksum = "a2bd12c1caf447e69cd4528f47f94d203fd2582878ecb9e9465484c4148a8223" [[package]] name = "camino" @@ -474,7 +474,7 @@ dependencies = [ "tar", "termcolor", "time", - "toml 0.7.6", + "toml 0.7.8", "url", "windows-sys 0.45.0", ] @@ -538,9 +538,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "chrono" -version = "0.4.28" +version = "0.4.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "95ed24df0632f708f5f6d8082675bef2596f7084dee3dd55f632290bf35bfe0f" +checksum = "7f2c685bad3eb3d45a01354cedb7d5faa66194d1d58ba6e267a8de788f79db38" dependencies = [ "android-tzdata", "iana-time-zone", @@ -550,9 +550,9 @@ dependencies = [ [[package]] name = "clap" -version = "4.4.2" +version = "4.4.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6a13b88d2c62ff462f88e4a121f17a82c1af05693a2f192b5c38d14de73c19f6" +checksum = "b1d7b8d5ec32af0fadc644bf1fd509a688c2103b185644bb1e29d164e0703136" dependencies = [ "clap_builder", "clap_derive", @@ -560,9 +560,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.4.2" +version = "4.4.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2bb9faaa7c2ef94b2743a21f5a29e6f0010dff4caa69ac8e9d6cf8b6fa74da08" +checksum = "5179bb514e4d7c2051749d8fcefa2ed6d06a9f4e6d69faf3805f5d80b8cf8d56" dependencies = [ "anstream", "anstyle", @@ -579,7 +579,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -834,9 +834,9 @@ dependencies = [ [[package]] name = "crypto-bigint" -version = "0.5.2" +version = "0.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cf4c2f4e1afd912bc40bfd6fed5d9dc1f288e0ba01bfcc835cc5bc3eb13efe15" +checksum = "740fe28e594155f10cfc383984cbefd529d7396050557148f79cb0f621204124" dependencies = [ "generic-array", "rand_core", @@ -908,9 +908,9 @@ dependencies = [ [[package]] name = "curl-sys" -version = "0.4.65+curl-8.2.1" +version = "0.4.66+curl-8.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "961ba061c9ef2fe34bbd12b807152d96f0badd2bebe7b90ce6c8c8b7572a0986" +checksum = "70c44a72e830f0e40ad90dda8a6ab6ed6314d39776599a58a2e5e37fbc6db5b9" dependencies = [ "cc", "libc", @@ -918,7 +918,7 @@ dependencies = [ "openssl-sys", "pkg-config", "vcpkg", - "winapi", + "windows-sys 0.48.0", ] [[package]] @@ -1214,9 +1214,9 @@ dependencies = [ [[package]] name = "fiat-crypto" -version = "0.1.20" +version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e825f6987101665dea6ec934c09ec6d721de7bc1bf92248e1d5810c8cd636b77" +checksum = "d0870c84016d4b481be5c9f323c24f65e31e901ae618f0e80f4308fb00de1d2d" [[package]] name = "filetime" @@ -1352,7 +1352,7 @@ checksum = "89ca545a94061b6365f2c7355b4b32bd20df3ff95f02da9329b34ccc3bd6ee72" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -1508,7 +1508,7 @@ version = "0.3.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "06683b93020a07e3dbcf5f8c0f6d40080d725bea7936fc01ad345c01b97dc270" dependencies = [ - "base64 0.21.3", + "base64 0.21.4", "bytes", "headers-core", "http", @@ -1754,7 +1754,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cb0889898416213fab133e1d33a0e5858a48177452750691bde3666d0fdbaf8b" dependencies = [ "hermit-abi", - "rustix 0.38.11", + "rustix 0.38.13", "windows-sys 0.48.0", ] @@ -1860,9 +1860,9 @@ checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" [[package]] name = "libc" -version = "0.2.147" +version = "0.2.148" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4668fb0ea861c1df094127ac5f1da3409a82116a4ba74fca2e58ef927159bb3" +checksum = "9cdc71e17332e86d2e1d38c1f99edcb6288ee11b815fb1a4b049eaa2114d369b" [[package]] name = "libgit2-sys" @@ -1918,9 +1918,9 @@ checksum = "ef53942eb7bf7ff43a617b3e2c1c4a5ecf5944a7c1bc12d7ee39bbb15e5c1519" [[package]] name = "linux-raw-sys" -version = "0.4.5" +version = "0.4.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503" +checksum = "1a9bad9f94746442c783ca431b22403b519cd7fbeed0533fdd6328b2f2212128" [[package]] name = "log" @@ -2174,7 +2174,7 @@ checksum = "a948666b637a0f465e8564c73e89d4dde00d72d4d473cc972f390fc3dcee7d9c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -2185,9 +2185,9 @@ checksum = "ff011a302c396a5197692431fc1948019154afc178baf7d8e37367442a4601cf" [[package]] name = "openssl-sys" -version = "0.9.92" +version = "0.9.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "db7e971c2c2bba161b2d2fdf37080177eff520b3bc044787c7f1f5f9e78d869b" +checksum = "db4d56a4c0478783083cfafcc42493dd4a981d41669da64b4572a2a089b51b1d" dependencies = [ "cc", "libc", @@ -2207,9 +2207,9 @@ dependencies = [ [[package]] name = "orion" -version = "0.17.5" +version = "0.17.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b11468cc6afd61a126fe3f91cc4cc8a0dbe7917d0a4b5e8357ba91cc47444462" +checksum = "7abdb10181903c8c4b016ba45d6d6d5af1a1e2a461aa4763a83b87f5df4695e5" dependencies = [ "fiat-crypto", "subtle", @@ -2328,7 +2328,7 @@ dependencies = [ "pest_meta", "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -2359,7 +2359,7 @@ checksum = "4359fd9c9171ec6e8c62926d6faaf553a8dc3f64e1507e76da7911b4f6a04405" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -2448,9 +2448,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.66" +version = "1.0.67" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18fb31db3f9bddb2ea821cde30a9f70117e3f119938b5ee630b7403aa6e2ead9" +checksum = "3d433d9f1a3e8c1263d9456598b16fec66f4acc9a74dacffd35c7bb09b3a1328" dependencies = [ "unicode-ident", ] @@ -2602,7 +2602,7 @@ dependencies = [ "nix 0.27.1", "rustc-hash", "serde", - "toml 0.7.6", + "toml 0.7.8", "uuid", "walkdir", "winapi", @@ -2786,7 +2786,7 @@ version = "0.11.20" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3e9ad3fe7488d7e34558a2033d45a0c90b72d97b4f80705666fea71472e2e6a1" dependencies = [ - "base64 0.21.3", + "base64 0.21.4", "bytes", "encoding_rs", "futures-core", @@ -2914,14 +2914,14 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.11" +version = "0.38.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c0c3dde1fc030af041adc40e79c0e7fbcf431dd24870053d187d7c66e4b87453" +checksum = "d7db8590df6dfcd144d22afd1b83b36c21a18d7cbc1dc4bb5295a8712e9eb662" dependencies = [ "bitflags 2.4.0", "errno", "libc", - "linux-raw-sys 0.4.5", + "linux-raw-sys 0.4.7", "windows-sys 0.48.0", ] @@ -2933,7 +2933,7 @@ checksum = "cd8d6c9f025a446bc4d18ad9632e69aec8f287aa84499ee335599fabd20c3fd8" dependencies = [ "log", "ring", - "rustls-webpki 0.101.4", + "rustls-webpki 0.101.5", "sct", ] @@ -2943,14 +2943,14 @@ version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2d3987094b1d07b653b7dfdc3f70ce9a1da9c51ac18c1b06b662e4f9a0e9f4b2" dependencies = [ - "base64 0.21.3", + "base64 0.21.4", ] [[package]] name = "rustls-webpki" -version = "0.100.2" +version = "0.100.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e98ff011474fa39949b7e5c0428f9b4937eda7da7848bbb947786b7be0b27dab" +checksum = "5f6a5fc258f1c1276dfe3016516945546e2d5383911efc0fc4f1cdc5df3a4ae3" dependencies = [ "ring", "untrusted", @@ -2958,9 +2958,9 @@ dependencies = [ [[package]] name = "rustls-webpki" -version = "0.101.4" +version = "0.101.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7d93931baf2d282fff8d3a532bbfd7653f734643161b87e3e01e59a04439bf0d" +checksum = "45a27e3b59326c16e23d30aeb7a36a24cc0d29e71d68ff611cdfb4a01d013bed" dependencies = [ "ring", "untrusted", @@ -3114,14 +3114,14 @@ checksum = "4eca7ac642d82aa35b60049a6eccb4be6be75e599bd2e9adb5f875a737654af2" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] name = "serde_json" -version = "1.0.105" +version = "1.0.107" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "693151e1ac27563d6dbcec9dee9fbd5da8539b20fa14ad3752b2e6d363ace360" +checksum = "6b420ce6e3d8bd882e9b243c6eed35dbc9a6110c9769e74b584e0d68d1f20c65" dependencies = [ "itoa", "ryu", @@ -3283,9 +3283,9 @@ dependencies = [ [[package]] name = "socket2" -version = "0.5.3" +version = "0.5.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2538b18701741680e0322a2302176d3253a35388e2e62f172f64f4f16605f877" +checksum = "4031e820eb552adee9295814c0ced9e5cf38ddf1e8b7d566d6de8e2538ea989e" dependencies = [ "libc", "windows-sys 0.48.0", @@ -3338,9 +3338,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.31" +version = "2.0.37" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "718fa2415bcb8d8bd775917a1bf12a7931b6dfa890753378538118181e0cb398" +checksum = "7303ef2c05cd654186cb250d29049a24840ca25d2747c25c0381c8d9e2f582e8" dependencies = [ "proc-macro2", "quote", @@ -3392,7 +3392,7 @@ dependencies = [ "cfg-if", "fastrand 2.0.0", "redox_syscall 0.3.5", - "rustix 0.38.11", + "rustix 0.38.13", "windows-sys 0.48.0", ] @@ -3409,9 +3409,9 @@ dependencies = [ [[package]] name = "termcolor" -version = "1.2.0" +version = "1.3.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "be55cf8942feac5c765c2c993422806843c9a9a45d4d5c407ad6dd2ea95eb9b6" +checksum = "6093bad37da69aab9d123a8091e4be0aa4a03e4d601ec641c327398315f62b64" dependencies = [ "winapi-util", ] @@ -3431,7 +3431,7 @@ dependencies = [ "prusti-launch", "rustwide", "serde", - "toml 0.7.6", + "toml 0.7.8", ] [[package]] @@ -3464,7 +3464,7 @@ checksum = "49922ecae66cc8a249b77e68d1d0623c1b2c514f0060c27cdc68bd62a1219d35" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -3533,7 +3533,7 @@ dependencies = [ "num_cpus", "pin-project-lite", "signal-hook-registry", - "socket2 0.5.3", + "socket2 0.5.4", "windows-sys 0.48.0", ] @@ -3595,9 +3595,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.7.6" +version = "0.7.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c17e963a819c331dcacd7ab957d80bc2b9a9c1e71c804826d2f283dd65306542" +checksum = "dd79e69d3b627db300ff956027cc6c3798cef26d22526befdfcd12feeb6d2257" dependencies = [ "serde", "serde_spanned", @@ -3616,9 +3616,9 @@ dependencies = [ [[package]] name = "toml_edit" -version = "0.19.14" +version = "0.19.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8123f27e969974a3dfba720fdb560be359f57b44302d280ba72e76a74480e8a" +checksum = "1b5bb770da30e5cbfde35a2d7b9b8a2c4b8ef89548a7a6aeab5c9a576e3e7421" dependencies = [ "indexmap 2.0.0", "serde", @@ -3662,7 +3662,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", ] [[package]] @@ -3752,9 +3752,9 @@ dependencies = [ [[package]] name = "typenum" -version = "1.16.0" +version = "1.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "497961ef93d974e23eb6f433eb5fe1b7930b659f06d12dec6fc44a8f554c0bba" +checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" [[package]] name = "ucd-trie" @@ -3806,9 +3806,9 @@ checksum = "92888ba5573ff080736b3648696b70cafad7d250551175acbaa4e0385b3e1460" [[package]] name = "unicode-ident" -version = "1.0.11" +version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "301abaae475aa91687eb82514b328ab47a211a533026cb25fc3e519b86adfc3c" +checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b" [[package]] name = "unicode-normalization" @@ -3843,12 +3843,12 @@ version = "2.7.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0b11c96ac7ee530603dcdf68ed1557050f374ce55a5a07193ebf8cbc9f8927e9" dependencies = [ - "base64 0.21.3", + "base64 0.21.4", "flate2", "log", "once_cell", "rustls", - "rustls-webpki 0.100.2", + "rustls-webpki 0.100.3", "url", "webpki-roots 0.23.1", ] @@ -3992,9 +3992,9 @@ checksum = "9d5b2c62b4012a3e1eca5a7e077d13b3bf498c4073e33ccd58626607748ceeca" [[package]] name = "walkdir" -version = "2.3.3" +version = "2.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36df944cda56c7d8d8b7496af378e6b16de9284591917d307c9b4d313c44e698" +checksum = "d71d857dc86794ca4c280d616f7da00d2dbfd8cd788846559a6813e6aa4b54ee" dependencies = [ "same-file", "winapi-util", @@ -4067,7 +4067,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", "wasm-bindgen-shared", ] @@ -4101,7 +4101,7 @@ checksum = "54681b18a46765f095758388f2d0cf16eb8d4169b639ab575a8f5693af210c7b" dependencies = [ "proc-macro2", "quote", - "syn 2.0.31", + "syn 2.0.37", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -4128,7 +4128,7 @@ version = "0.23.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b03058f88386e5ff5310d9111d53f48b17d732b401aeb83a8d5190f2ac459338" dependencies = [ - "rustls-webpki 0.100.2", + "rustls-webpki 0.100.3", ] [[package]] diff --git a/analysis/src/bin/analysis-driver.rs b/analysis/src/bin/analysis-driver.rs index 51d8f083669..75f27dd4a33 100644 --- a/analysis/src/bin/analysis-driver.rs +++ b/analysis/src/bin/analysis-driver.rs @@ -147,7 +147,6 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { fn after_analysis<'tcx>( &mut self, - _error_handler: &EarlyErrorHandler, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { diff --git a/analysis/src/bin/gen-accessibility-driver.rs b/analysis/src/bin/gen-accessibility-driver.rs index 6d0b18486d9..832d0f421e1 100644 --- a/analysis/src/bin/gen-accessibility-driver.rs +++ b/analysis/src/bin/gen-accessibility-driver.rs @@ -99,7 +99,6 @@ impl prusti_rustc_interface::driver::Callbacks for OurCompilerCalls { fn after_analysis<'tcx>( &mut self, - _error_handler: &EarlyErrorHandler, compiler: &interface::Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { diff --git a/analysis/tests/test_cases/definitely_initialized/abs.stdout b/analysis/tests/test_cases/definitely_initialized/abs.stdout index 02b924954e9..47c616c43a8 100644 --- a/analysis/tests/test_cases/definitely_initialized/abs.stdout +++ b/analysis/tests/test_cases/definitely_initialized/abs.stdout @@ -45,14 +45,6 @@ Result for function abs(): "_6" ], "statement: _5 = Ge(move _6, const 0_i32)" - ], - [ - "state:", - [ - "_1", - "_5" - ], - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -78,6 +70,13 @@ Result for function abs(): ], "bb1": [ [ + [ + "state:", + [ + "_1" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ @@ -137,6 +136,13 @@ Result for function abs(): ], "bb2": [ [ + [ + "state:", + [ + "_1" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ diff --git a/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout b/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout index c8b57b13729..87be870a5e5 100644 --- a/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout +++ b/analysis/tests/test_cases/definitely_initialized/repeated_assignment.stdout @@ -131,15 +131,6 @@ Result for function main(): "_6" ], "statement: _5 = Gt(move _6, const 2_i32)" - ], - [ - "state:", - [ - "_1", - "_2", - "_5" - ], - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -168,6 +159,14 @@ Result for function main(): ], "bb2": [ [ + [ + "state:", + [ + "_1", + "_2" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ @@ -205,6 +204,14 @@ Result for function main(): ], "bb3": [ [ + [ + "state:", + [ + "_1", + "_2" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ diff --git a/analysis/tests/test_cases/reaching_definitions/abs.stdout b/analysis/tests/test_cases/reaching_definitions/abs.stdout index 90086fab2fe..2aab0969c4c 100644 --- a/analysis/tests/test_cases/reaching_definitions/abs.stdout +++ b/analysis/tests/test_cases/reaching_definitions/abs.stdout @@ -59,21 +59,6 @@ Result for function abs(): ] }, "statement: _5 = Ge(move _6, const 0_i32)" - ], - [ - "state:", - { - "_1": [ - "arg0" - ], - "_5": [ - "bb0[5]: _5 = Ge(move _6, const 0_i32)" - ], - "_6": [ - "bb0[4]: _6 = _1" - ] - }, - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -122,6 +107,21 @@ Result for function abs(): ], "bb1": [ [ + [ + "state:", + { + "_1": [ + "arg0" + ], + "_5": [ + "bb0[5]: _5 = Ge(move _6, const 0_i32)" + ], + "_6": [ + "bb0[4]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -165,7 +165,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "statement: _3 = move _7" @@ -177,7 +177,7 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -186,7 +186,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "statement: StorageDead(_7)" @@ -198,7 +198,7 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -207,7 +207,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "statement: _4 = const ()" @@ -219,10 +219,10 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_4": [ - "bb1[4]: _4 = const ()" + "bb1[5]: _4 = const ()" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -231,7 +231,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] }, "terminator: goto -> bb4", @@ -243,10 +243,10 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7" + "bb1[3]: _3 = move _7" ], "_4": [ - "bb1[4]: _4 = const ()" + "bb1[5]: _4 = const ()" ], "_5": [ "bb0[5]: _5 = Ge(move _6, const 0_i32)" @@ -255,7 +255,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ] } ] @@ -263,6 +263,21 @@ Result for function abs(): ], "bb2": [ [ + [ + "state:", + { + "_1": [ + "arg0" + ], + "_5": [ + "bb0[5]: _5 = Ge(move _6, const 0_i32)" + ], + "_6": [ + "bb0[4]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -306,7 +321,7 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ] }, "statement: _9 = Eq(_8, const i32::MIN)" @@ -324,10 +339,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: assert(!move _9, /"attempt to negate `{}`, which would overflow/", _8) -> [success: bb3, unwind: bb5]", @@ -345,10 +360,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] } ], @@ -365,10 +380,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] } ] @@ -389,10 +404,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: _3 = Neg(move _8)" @@ -413,10 +428,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_8)" @@ -437,10 +452,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: _4 = const ()" @@ -464,10 +479,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: goto -> bb4", @@ -491,10 +506,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] } ] @@ -509,11 +524,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -523,13 +538,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_5)" @@ -541,11 +556,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -555,13 +570,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_4)" @@ -573,11 +588,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -587,13 +602,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: _0 = _3" @@ -608,11 +623,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -622,13 +637,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "statement: StorageDead(_3)" @@ -643,11 +658,11 @@ Result for function abs(): "arg0" ], "_3": [ - "bb1[2]: _3 = move _7", + "bb1[3]: _3 = move _7", "bb3[0]: _3 = Neg(move _8)" ], "_4": [ - "bb1[4]: _4 = const ()", + "bb1[5]: _4 = const ()", "bb3[2]: _4 = const ()" ], "_5": [ @@ -657,13 +672,13 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_7": [ - "bb1[1]: _7 = _1" + "bb1[2]: _7 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: return", @@ -683,10 +698,10 @@ Result for function abs(): "bb0[4]: _6 = _1" ], "_8": [ - "bb2[1]: _8 = _1" + "bb2[2]: _8 = _1" ], "_9": [ - "bb2[2]: _9 = Eq(_8, const i32::MIN)" + "bb2[3]: _9 = Eq(_8, const i32::MIN)" ] }, "terminator: resume", diff --git a/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout b/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout index 32acc0cbcea..8358364481a 100644 --- a/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout +++ b/analysis/tests/test_cases/reaching_definitions/repeated_assignment.stdout @@ -215,27 +215,6 @@ Result for function main(): ] }, "statement: _5 = Gt(move _6, const 2_i32)" - ], - [ - "state:", - { - "_1": [ - "bb1[0]: _1 = move _3" - ], - "_2": [ - "bb0[4]: _2 = const 3_i32" - ], - "_3": [ - "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" - ], - "_5": [ - "bb1[6]: _5 = Gt(move _6, const 2_i32)" - ], - "_6": [ - "bb1[5]: _6 = _1" - ] - }, - "statement: StorageDead(_6)" ] ], "state before terminator:", @@ -302,6 +281,27 @@ Result for function main(): ], "bb2": [ [ + [ + "state:", + { + "_1": [ + "bb1[0]: _1 = move _3" + ], + "_2": [ + "bb0[4]: _2 = const 3_i32" + ], + "_3": [ + "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" + ], + "_5": [ + "bb1[6]: _5 = Gt(move _6, const 2_i32)" + ], + "_6": [ + "bb1[5]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -330,7 +330,7 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32" + "bb2[1]: _2 = const 5_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" @@ -351,13 +351,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32" + "bb2[1]: _2 = const 5_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()" + "bb2[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -375,13 +375,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32" + "bb2[1]: _2 = const 5_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()" + "bb2[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -395,6 +395,27 @@ Result for function main(): ], "bb3": [ [ + [ + "state:", + { + "_1": [ + "bb1[0]: _1 = move _3" + ], + "_2": [ + "bb0[4]: _2 = const 3_i32" + ], + "_3": [ + "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" + ], + "_5": [ + "bb1[6]: _5 = Gt(move _6, const 2_i32)" + ], + "_6": [ + "bb1[5]: _6 = _1" + ] + }, + "statement: StorageDead(_6)" + ], [ "state:", { @@ -423,7 +444,7 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb3[0]: _2 = const 7_i32" + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" @@ -444,13 +465,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb3[0]: _2 = const 7_i32" + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb3[1]: _4 = const ()" + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -468,13 +489,13 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb3[0]: _2 = const 7_i32" + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb3[1]: _4 = const ()" + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -495,15 +516,15 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32", - "bb3[0]: _2 = const 7_i32" + "bb2[1]: _2 = const 5_i32", + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -521,15 +542,15 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32", - "bb3[0]: _2 = const 7_i32" + "bb2[1]: _2 = const 5_i32", + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -547,15 +568,15 @@ Result for function main(): "bb1[0]: _1 = move _3" ], "_2": [ - "bb2[0]: _2 = const 5_i32", - "bb3[0]: _2 = const 7_i32" + "bb2[1]: _2 = const 5_i32", + "bb3[1]: _2 = const 7_i32" ], "_3": [ "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -579,8 +600,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -607,8 +628,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -635,8 +656,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" @@ -663,8 +684,8 @@ Result for function main(): "bb0[7]: _3 = input() -> [return: bb1, unwind: bb5]" ], "_4": [ - "bb2[1]: _4 = const ()", - "bb3[1]: _4 = const ()" + "bb2[2]: _4 = const ()", + "bb3[2]: _4 = const ()" ], "_5": [ "bb1[6]: _5 = Gt(move _6, const 2_i32)" diff --git a/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout b/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout index e5a0337d009..3aee1e2dff8 100644 --- a/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout +++ b/analysis/tests/test_cases/relaxed_definitely_initialized/abs.stdout @@ -45,21 +45,13 @@ Result for function abs(): "_6" ], "statement: _5 = Ge(move _6, const 0_i32)" - ], - [ - "state:", - [ - "_1", - "_5", - "_6" - ], - "statement: StorageDead(_6)" ] ], "state before terminator:", [ "_1", - "_5" + "_5", + "_6" ], "terminator: switchInt(move _5) -> [0: bb2, otherwise: bb1]", { @@ -67,20 +59,31 @@ Result for function abs(): "state:", [ "_1", - "_5" + "_5", + "_6" ] ], "bb2": [ "state:", [ "_1", - "_5" + "_5", + "_6" ] ] } ], "bb1": [ [ + [ + "state:", + [ + "_1", + "_5", + "_6" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ @@ -148,6 +151,15 @@ Result for function abs(): ], "bb2": [ [ + [ + "state:", + [ + "_1", + "_5", + "_6" + ], + "statement: StorageDead(_6)" + ], [ "state:", [ diff --git a/prusti-interface/src/specs/external.rs b/prusti-interface/src/specs/external.rs index 7568ed85692..0e5fc8fb1a4 100644 --- a/prusti-interface/src/specs/external.rs +++ b/prusti-interface/src/specs/external.rs @@ -177,11 +177,11 @@ impl<'tcx> ExternSpecResolver<'tcx> { let (resolved_gens, current_gens) = ( self.env_query .identity_substs(resolved_def_id) - .non_erasable_generics() + .non_erasable_generics(self.env_query.tcx(), resolved_def_id) .count(), self.env_query .identity_substs(current_def_id) - .non_erasable_generics() + .non_erasable_generics(self.env_query.tcx(), current_def_id) .count(), ); if resolved_gens != current_gens { diff --git a/prusti-tests/tests/runtime_checks/fail/predicates/nested-predicate b/prusti-tests/tests/runtime_checks/fail/predicates/nested-predicate deleted file mode 100755 index bca4865c9bb..00000000000 Binary files a/prusti-tests/tests/runtime_checks/fail/predicates/nested-predicate and /dev/null differ diff --git a/prusti-tests/tests/runtime_checks/pass/assert-assume-invariant/assert-old b/prusti-tests/tests/runtime_checks/pass/assert-assume-invariant/assert-old deleted file mode 100755 index 56de82ee6f1..00000000000 Binary files a/prusti-tests/tests/runtime_checks/pass/assert-assume-invariant/assert-old and /dev/null differ diff --git a/prusti-tests/tests/verify/ui/failing-postcondition.stderr b/prusti-tests/tests/verify/ui/failing-postcondition.stderr index 54424aa4380..722f605d454 100644 --- a/prusti-tests/tests/verify/ui/failing-postcondition.stderr +++ b/prusti-tests/tests/verify/ui/failing-postcondition.stderr @@ -1,8 +1,8 @@ error: [Prusti: verification error] postcondition might not hold. - --> $DIR/failing-postcondition.rs:8:11 + --> $DIR/failing-postcondition.rs:8:31 | 8 | #[ensures(something_true() && false)] - | ^^^^^^^^^^^^^^^^^^^^^^^^^ + | ^^^^^ | note: the error originates here --> $DIR/failing-postcondition.rs:9:1 diff --git a/prusti-tests/tests/verify_overflow/fail/index-vec.rs b/prusti-tests/tests/verify_overflow/fail/index-vec.rs index 04929897555..0e2b1a6e446 100644 --- a/prusti-tests/tests/verify_overflow/fail/index-vec.rs +++ b/prusti-tests/tests/verify_overflow/fail/index-vec.rs @@ -3,7 +3,7 @@ use prusti_contracts::*; #[pure] fn get_third(v: &Vec) -> u32 { v[2] //~ ERROR Using usize as index/range type for &std::vec::Vec is not currently supported in pure functions - //~^ ERROR Non-slice LHS type '&u32' not supported yet + //~^ ERROR Non-slice LHS type } fn main(){} diff --git a/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs b/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs index 8978d1d3174..a76476ac167 100644 --- a/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs +++ b/prusti-viper/src/encoder/mir/procedures/encoder/ghost.rs @@ -51,12 +51,12 @@ impl<'a, 'p, 'v, 'tcx> GhostChecker<'a, 'p, 'v, 'tcx> { let ty = &self.p.mir.local_decls[*local].ty; let ty_str = format!("{ty:?}"); - let ghost_tys = ["Ghost", "Int", "Seq", "Map"]; - - for ghost in ghost_tys { - if ty_str.starts_with(&format!("prusti_contracts::{ghost}")) { - return true; - } + match &ty_str { + _ if ty_str.starts_with("Adt(prusti_contracts::Ghost,") => return true, + _ if ty_str.starts_with("Adt(prusti_contracts::Int,") => return true, + _ if ty_str.starts_with("Adt(prusti_contracts::Seq,") => return true, + _ if ty_str.starts_with("Adt(prusti_contracts::Map,") => return true, + _ => {} } // unit types get generated all over, and carry no information, thus okay to leak outside the ghost block diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs index 67f838df495..50619f97f49 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_poly.rs @@ -82,12 +82,14 @@ pub(super) fn inline_spec_item<'tcx>( ) -> SpannedEncodingResult { // each non-lifetime parameter should be matched with a subst assert_eq!( - substs.non_erasable_generics().count(), + substs + .non_erasable_generics(encoder.env().tcx(), def_id) + .count(), encoder .env() .query .identity_substs(def_id) - .non_erasable_generics() + .non_erasable_generics(encoder.env().tcx(), def_id) .count() ); diff --git a/prusti-viper/src/encoder/procedure_encoder.rs b/prusti-viper/src/encoder/procedure_encoder.rs index e64982df160..598245fcd98 100644 --- a/prusti-viper/src/encoder/procedure_encoder.rs +++ b/prusti-viper/src/encoder/procedure_encoder.rs @@ -2488,7 +2488,7 @@ impl<'p, 'v: 'p, 'tcx: 'v> ProcedureEncoder<'p, 'v, 'tcx> { .. } => { let ty = literal.ty(); - let func_const_val = literal.try_to_value(self.encoder.env().tcx()); + let func_const_val = literal.try_to_scalar_int(); if let ty::TyKind::FnDef(called_def_id, call_substs) = ty.kind() { let called_def_id = *called_def_id; debug!("Encode function call {:?} with substs {:?}", called_def_id, call_substs); diff --git a/prusti/src/callbacks.rs b/prusti/src/callbacks.rs index 8339cab83db..c163d9a7aa5 100644 --- a/prusti/src/callbacks.rs +++ b/prusti/src/callbacks.rs @@ -20,7 +20,7 @@ use prusti_rustc_interface::{ }, mir_build, mir_transform::{self, inline}, - session::{EarlyErrorHandler, Session}, + session::Session, span::def_id::{DefId, LocalDefId, LOCAL_CRATE}, trait_selection::traits, }; @@ -240,7 +240,6 @@ impl prusti_rustc_interface::driver::Callbacks for PrustiCompilerCalls { #[tracing::instrument(level = "debug", skip_all)] fn after_analysis<'tcx>( &mut self, - _error_handler: &EarlyErrorHandler, compiler: &Compiler, queries: &'tcx Queries<'tcx>, ) -> Compilation { diff --git a/rust-toolchain b/rust-toolchain index 35315b86c9c..4439ba166b4 100644 --- a/rust-toolchain +++ b/rust-toolchain @@ -1,4 +1,4 @@ [toolchain] -channel = "nightly-2023-09-01" +channel = "nightly-2023-09-15" components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt", "clippy" ] profile = "minimal" diff --git a/viper/src/cache.rs b/viper/src/cache.rs index 4ed6eb89561..4b78dc3d1fc 100644 --- a/viper/src/cache.rs +++ b/viper/src/cache.rs @@ -27,7 +27,7 @@ pub struct PersistentCache { data: FxHashMap, } -const RESULT_CACHE_VERSION: u64 = 3; +const RESULT_CACHE_VERSION: u64 = 4; #[derive(Debug, serde::Serialize, serde::Deserialize)] struct ResultCache { diff --git a/vir/defs/polymorphic/ast/common.rs b/vir/defs/polymorphic/ast/common.rs index 71abe8eeabb..c27081c6be5 100644 --- a/vir/defs/polymorphic/ast/common.rs +++ b/vir/defs/polymorphic/ast/common.rs @@ -95,7 +95,7 @@ impl fmt::Display for PermAmount { } } -#[allow(clippy::incorrect_partial_ord_impl_on_ord_type)] +#[allow(clippy::non_canonical_partial_ord_impl)] impl PartialOrd for PermAmount { fn partial_cmp(&self, other: &PermAmount) -> Option { match (self, other) {