search

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.55k stars 106 forks source link

Prusti cannot detect that a generic type fulfills the Copy trait bound requirement #1453

Closed Ramla-I closed 1 year ago

Ramla-I commented 1 year ago

I'm trying to write a function which takes a generic linked list as an argument which is instantiated with a generic type. I get the error message: [Prusti: invalid specification] return type of pure function does not implement Copy which is incorrect because the trait bounds specify that the type must implement Copy, and the type does.

Specifically, this function verifies:

fn can_create_new(chunk_range: Range, chunk_list: &mut List<Range>) -> Result<(), usize> {
    let overlap_idx = chunk_list.elem_overlaps_in_list(chunk_range, 0);
    if overlap_idx.is_some(){
        Err(overlap_idx.unwrap())
    } else {
        chunk_list.push(chunk_range);
        Ok(())
    }
}

but this one does not:

fn can_create_new<U: Copy + PartialOrd>(chunk_range: Range<U>, chunk_list: &mut List<Range<U>>) -> Result<(), usize> {
    let overlap_idx = chunk_list.elem_overlaps_in_list(chunk_range, 0);
    if overlap_idx.is_some(){
        Err(overlap_idx.unwrap())
    } else {
        chunk_list.push(chunk_range);
        Ok(())
    }
}

The complete code is here: https://github.com/Ramla-I/generic_linked_list

The Prusti assistant output is:

Run verification on /home/ramla/Projects/generic_linked_list/src/main.rs...
Preparing verification run #60.
Killing 0 processes.
Run command '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/Latest/prusti/cargo-prusti --message-format=json'
Spawned PID: 440987
Output from '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/Latest/prusti/cargo-prusti --message-format=json' (1.6s):
┌──── Begin stdout ────┐
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.66 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/build.rs","edition":"2021","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/build/proc-macro2-3b1d99ed0729713f/build-script-build"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"libc 0.2.147 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/build.rs","edition":"2015","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/build/libc-601a4d5d632627d9/build-script-build"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"libc 0.2.147 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":["freebsd11","libc_priv_mod_use","libc_union","libc_const_size_of","libc_align","libc_int128","libc_core_cvoid","libc_packedN","libc_cfg_target_vendor","libc_non_exhaustive","libc_long_array","libc_ptr_addr_of","libc_underscore_const_names","libc_const_extern_fn"],"env":[],"out_dir":"/home/ramla/Projects/generic_linked_list/target/verify/debug/build/libc-7725fee117739437/out"}
{"reason":"build-script-executed","package_id":"proc-macro2 1.0.66 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":["wrap_proc_macro","proc_macro_span"],"env":[],"out_dir":"/home/ramla/Projects/generic_linked_list/target/verify/debug/build/proc-macro2-286d68bd17fda1bc/out"}
{"reason":"compiler-artifact","package_id":"unicode-ident 1.0.11 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/unicode-ident-1.0.11/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"unicode-ident","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/unicode-ident-1.0.11/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libunicode_ident-27c541bdd3194d90.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libunicode_ident-27c541bdd3194d90.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"libc 0.2.147 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"libc","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/liblibc-ff82d7394b050f54.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/liblibc-ff82d7394b050f54.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"syn 1.0.109 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["clone-impls","default","derive","extra-traits","full","parsing","printing","proc-macro","quote","visit","visit-mut"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/build/syn-e846c4791d691919/build-script-build"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"cfg-if 1.0.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/cfg-if-1.0.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"cfg-if","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/cfg-if-1.0.0/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libcfg_if-164bf69dabbcc49a.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libcfg_if-164bf69dabbcc49a.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.66 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"proc-macro2","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/proc-macro2-1.0.66/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libproc_macro2-c308a930a0e3b3ae.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libproc_macro2-c308a930a0e3b3ae.rmeta"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"syn 1.0.109 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":[],"env":[],"out_dir":"/home/ramla/Projects/generic_linked_list/target/verify/debug/build/syn-da4a3482c8d0d853/out"}
{"reason":"compiler-artifact","package_id":"getrandom 0.2.10 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/getrandom-0.2.10/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"getrandom","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/getrandom-0.2.10/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libgetrandom-4075de1469943232.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libgetrandom-4075de1469943232.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"either 1.9.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/either-1.9.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"either","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/either-1.9.0/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["use_std"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libeither-8b44e017d5365072.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libeither-8b44e017d5365072.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"rustc-hash 1.1.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/rustc-hash-1.1.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"rustc-hash","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/rustc-hash-1.1.0/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","std"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/librustc_hash-cd2cf40ce95ec4e2.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/librustc_hash-cd2cf40ce95ec4e2.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"quote 1.0.33 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/quote-1.0.33/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"quote","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/quote-1.0.33/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libquote-1425e0fbf51b7cbe.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libquote-1425e0fbf51b7cbe.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"uuid 1.4.1 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/uuid-1.4.1/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"uuid","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/uuid-1.4.1/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","getrandom","rng","std","v4"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libuuid-b75b903a080b9a16.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libuuid-b75b903a080b9a16.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"itertools 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/itertools-0.11.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"itertools","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/itertools-0.11.0/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":false},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","use_alloc","use_std"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libitertools-85f8fc9b149b66e1.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libitertools-85f8fc9b149b66e1.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"syn 1.0.109 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"syn","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/syn-1.0.109/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["clone-impls","default","derive","extra-traits","full","parsing","printing","proc-macro","quote","visit","visit-mut"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libsyn-b6354a40f4bbb8e8.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libsyn-b6354a40f4bbb8e8.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-specs 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-specs-0.2.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-specs","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-specs-0.2.0/src/lib.rs","edition":"2021","doc":true,"doctest":false,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libprusti_specs-9c1041daefcefc70.rlib","/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libprusti_specs-9c1041daefcefc70.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts-proc-macros 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-proc-macros-0.2.0/Cargo.toml","target":{"kind":["proc-macro"],"crate_types":["proc-macro"],"name":"prusti-contracts-proc-macros","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-proc-macros-0.2.0/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":0,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["prusti"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libprusti_contracts_proc_macros-73b917a9d00350bc.so"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-0.2.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-contracts","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-contracts-0.2.0/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["prusti"],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libprusti_contracts-1df02524f0ad7c11.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-std 0.2.0 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-std-0.2.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-std","src_path":"/home/ramla/.cargo/registry/src/index.crates.io-6f17d22bba15001f/prusti-std-0.2.0/src/lib.rs","edition":"2021","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/generic_linked_list/target/verify/debug/deps/libprusti_std-d228200461121e33.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-message","package_id":"generic_linked_list 0.1.0 (path+file:///home/ramla/Projects/generic_linked_list)","manifest_path":"/home/ramla/Projects/generic_linked_list/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"generic_linked_list","src_path":"/home/ramla/Projects/generic_linked_list/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: unused variable: `other`\n  --> src/with_generic_type/range_generic.rs:17:24\n   |\n17 |     fn overlaps(&self, other: &Self) -> bool {\n   |                        ^^^^^ help: if this is intentional, prefix it with an underscore: `_other`\n   |\n   = note: `#[warn(unused_variables)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(unused_variables)]` on by default","rendered":null,"spans":[]},{"children":[],"code":null,"level":"help","message":"if this is intentional, prefix it with an underscore","rendered":null,"spans":[{"byte_end":479,"byte_start":474,"column_end":29,"column_start":24,"expansion":null,"file_name":"src/with_generic_type/range_generic.rs","is_primary":true,"label":null,"line_end":17,"line_start":17,"suggested_replacement":"_other","suggestion_applicability":"MachineApplicable","text":[{"highlight_end":29,"highlight_start":24,"text":"    fn overlaps(&self, other: &Self) -> bool {"}]}]}],"code":{"code":"unused_variables","explanation":null},"level":"warning","message":"unused variable: `other`","spans":[{"byte_end":479,"byte_start":474,"column_end":29,"column_start":24,"expansion":null,"file_name":"src/with_generic_type/range_generic.rs","is_primary":true,"label":null,"line_end":17,"line_start":17,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":29,"highlight_start":24,"text":"    fn overlaps(&self, other: &Self) -> bool {"}]}]}}
{"reason":"compiler-message","package_id":"generic_linked_list 0.1.0 (path+file:///home/ramla/Projects/generic_linked_list)","manifest_path":"/home/ramla/Projects/generic_linked_list/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"generic_linked_list","src_path":"/home/ramla/Projects/generic_linked_list/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"warning: comparison is useless due to type limits\n   --> src/with_generic_type/linked_list.rs:145:16\n    |\n145 |     #[requires(0 <= index && index <= self.len())]\n    |                ^^^^^^^^^^\n    |\n    = note: `#[warn(unused_comparisons)]` on by default\n\n","children":[{"children":[],"code":null,"level":"note","message":"`#[warn(unused_comparisons)]` on by default","rendered":null,"spans":[]}],"code":{"code":"unused_comparisons","explanation":null},"level":"warning","message":"comparison is useless due to type limits","spans":[{"byte_end":3963,"byte_start":3953,"column_end":26,"column_start":16,"expansion":null,"file_name":"src/with_generic_type/linked_list.rs","is_primary":true,"label":null,"line_end":145,"line_start":145,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":26,"highlight_start":16,"text":"    #[requires(0 <= index && index <= self.len())]"}]}]}}
{"reason":"compiler-message","package_id":"generic_linked_list 0.1.0 (path+file:///home/ramla/Projects/generic_linked_list)","manifest_path":"/home/ramla/Projects/generic_linked_list/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"generic_linked_list","src_path":"/home/ramla/Projects/generic_linked_list/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"error: [Prusti: invalid specification] return type of pure function does not implement Copy\n   --> src/with_generic_type/linked_list.rs:142:9\n    |\n142 |         link_lookup_copy(&self.head, index)\n    |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n\n","children":[],"code":null,"level":"error","message":"[Prusti: invalid specification] return type of pure function does not implement Copy","spans":[{"byte_end":3930,"byte_start":3895,"column_end":44,"column_start":9,"expansion":null,"file_name":"src/with_generic_type/linked_list.rs","is_primary":true,"label":null,"line_end":142,"line_start":142,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":44,"highlight_start":9,"text":"        link_lookup_copy(&self.head, index)"}]}]}}
{"reason":"compiler-message","package_id":"generic_linked_list 0.1.0 (path+file:///home/ramla/Projects/generic_linked_list)","manifest_path":"/home/ramla/Projects/generic_linked_list/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"generic_linked_list","src_path":"/home/ramla/Projects/generic_linked_list/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"error: aborting due to previous error; 2 warnings emitted\n\n","children":[],"code":null,"level":"error","message":"aborting due to previous error; 2 warnings emitted","spans":[]}}
{"reason":"build-finished","success":false}

└──── End stdout ──────┘
┌──── Begin stderr ────┐
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:25Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.055 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:26Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.578 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:25Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.018 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:25Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.413 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:26Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.097 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:25Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.144 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:25Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.028 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:25Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.195 seconds)
[2023-09-08T19:40:26Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:26Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.203 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:26Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (1.256 seconds)
[2023-09-08T19:40:25Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:30Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (4.413 seconds)
[2023-09-08T19:40:29Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:31Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (1.658 seconds)
[2023-09-08T19:40:31Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:32Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (1.232 seconds)
[2023-09-08T19:40:32Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:32Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.063 seconds)
[2023-09-08T19:40:32Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T19:40:32Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.029 seconds)
    Checking generic_linked_list v0.1.0 (/home/ramla/Projects/generic_linked_list)
[2023-09-08T21:37:05Z INFO  prusti_driver] Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC
[2023-09-08T21:37:05Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - external_spec::trusted_option::peek_option (generic_linked_list::external_spec::trusted_option::peek_option)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/external_spec/trusted_option.rs:40:1: 40:57 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - external_spec::trusted_option::peek_option_ref (generic_linked_list::external_spec::trusted_option::peek_option_ref)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/external_spec/trusted_option.rs:49:1: 49:56 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - external_spec::trusted_result::peek_result (generic_linked_list::external_spec::trusted_result::peek_result)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/external_spec/trusted_result.rs:8:1: 8:62 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - external_spec::trusted_result::peek_result_ref (generic_linked_list::external_spec::trusted_result::peek_result_ref)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/external_spec/trusted_result.rs:17:1: 17:61 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - external_spec::trusted_result::peek_err (generic_linked_list::external_spec::trusted_result::peek_err)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/external_spec/trusted_result.rs:26:1: 26:59 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - external_spec::trusted_result::peek_err_ref (generic_linked_list::external_spec::trusted_result::peek_err_ref)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/external_spec/trusted_result.rs:35:1: 35:58 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::link_lookup (generic_linked_list::with_generic_type::linked_list::link_lookup)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:124:1: 124:54 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::link_lookup_copy (generic_linked_list::with_generic_type::linked_list::link_lookup_copy)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:174:1: 174:71 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::link_len (generic_linked_list::with_generic_type::linked_list::link_len)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:188:1: 188:40 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::prusti_tests::_test_list (generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_list)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:199:5: 199:20 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::prusti_tests::_test_peek (generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_peek)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:223:5: 223:20 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::prusti_tests::_test_peek_mut (generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_peek_mut)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:236:5: 236:24 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::can_create_new (generic_linked_list::with_generic_type::can_create_new)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/mod.rs:9:1: 9:117 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - main (generic_linked_list::main)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/main.rs:11:1: 11:10 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <range_inclusive::RangeInclusive<Idx> as std::clone::Clone>::clone (generic_linked_list::range_inclusive::{impl#2}::clone)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/range_inclusive.rs:5:16: 5:21 (#50)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <range_inclusive::RangeInclusive<Idx> as std::cmp::PartialEq>::eq (generic_linked_list::range_inclusive::{impl#4}::eq)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/range_inclusive.rs:5:23: 5:32 (#51)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <range_inclusive::RangeInclusive<Idx> as std::cmp::Eq>::assert_receiver_is_total_eq (generic_linked_list::range_inclusive::{impl#6}::assert_receiver_is_total_eq)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/range_inclusive.rs:5:34: 5:36 (#52)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - range_inclusive::RangeInclusive::<Idx>::new (generic_linked_list::range_inclusive::{impl#0}::new)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/range_inclusive.rs:14:5: 14:58 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - range_inclusive::RangeInclusive::<Idx>::start (generic_linked_list::range_inclusive::{impl#0}::start)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/range_inclusive.rs:19:5: 19:38 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - range_inclusive::RangeInclusive::<Idx>::end (generic_linked_list::range_inclusive::{impl#0}::end)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/range_inclusive.rs:24:5: 24:36 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - range_inclusive::RangeInclusive::<Idx>::is_empty (generic_linked_list::range_inclusive::{impl#0}::is_empty)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/range_inclusive.rs:28:5: 28:35 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::len (generic_linked_list::with_generic_type::linked_list::{impl#0}::len)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:19:5: 19:31 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::is_empty (generic_linked_list::with_generic_type::linked_list::{impl#0}::is_empty)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:24:5: 24:31 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::new (generic_linked_list::with_generic_type::linked_list::{impl#0}::new)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:29:5: 29:25 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::lookup (generic_linked_list::with_generic_type::linked_list::{impl#0}::lookup)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:35:5: 35:45 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::push (generic_linked_list::with_generic_type::linked_list::{impl#0}::push)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:43:5: 43:36 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::head_removed (generic_linked_list::with_generic_type::linked_list::{impl#0}::head_removed)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:54:9: 54:52 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::try_pop (generic_linked_list::with_generic_type::linked_list::{impl#0}::try_pop)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:70:5: 70:43 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::pop (generic_linked_list::with_generic_type::linked_list::{impl#0}::pop)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:83:5: 83:31 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::peek (generic_linked_list::with_generic_type::linked_list::{impl#0}::peek)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:94:5: 94:29 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::peek_mut (generic_linked_list::with_generic_type::linked_list::{impl#0}::peek_mut)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:107:5: 107:41 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::lookup_copy (generic_linked_list::with_generic_type::linked_list::{impl#1}::lookup_copy)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:141:5: 141:49 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - with_generic_type::linked_list::List::<T>::elem_overlaps_in_list (generic_linked_list::with_generic_type::linked_list::{impl#1}::elem_overlaps_in_list)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/linked_list.rs:159:5: 159:87 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <with_generic_type::range_generic::Range<U> as std::clone::Clone>::clone (generic_linked_list::with_generic_type::range_generic::{impl#3}::clone)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/range_generic.rs:11:16: 11:21 (#178)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <with_generic_type::range_generic::Range<U> as std::cmp::PartialEq>::eq (generic_linked_list::with_generic_type::range_generic::{impl#5}::eq)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/range_generic.rs:11:23: 11:32 (#179)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <with_generic_type::range_generic::Range<U> as std::cmp::Eq>::assert_receiver_is_total_eq (generic_linked_list::with_generic_type::range_generic::{impl#7}::assert_receiver_is_total_eq)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/range_generic.rs:11:34: 11:36 (#180)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <with_generic_type::range_generic::Range<U> as with_generic_type::range_trait::UniqueCheck>::overlaps (generic_linked_list::with_generic_type::range_generic::{impl#0}::overlaps)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/range_generic.rs:17:5: 17:45 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]  - <with_generic_type::range_generic::Range<U> as std::ops::Deref>::deref (generic_linked_list::with_generic_type::range_generic::{impl#1}::deref)
[2023-09-08T21:37:05Z INFO  prusti_viper::verifier]    Source: src/with_generic_type/range_generic.rs:25:5: 25:42 (#0)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::external_spec::trusted_option::peek_option (generic_linked_list::external_spec::trusted_option::peek_option)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::external_spec::trusted_option::peek_option_ref (generic_linked_list::external_spec::trusted_option::peek_option_ref)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::external_spec::trusted_result::peek_result (generic_linked_list::external_spec::trusted_result::peek_result)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::external_spec::trusted_result::peek_result_ref (generic_linked_list::external_spec::trusted_result::peek_result_ref)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::external_spec::trusted_result::peek_err (generic_linked_list::external_spec::trusted_result::peek_err)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::external_spec::trusted_result::peek_err_ref (generic_linked_list::external_spec::trusted_result::peek_err_ref)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::with_generic_type::linked_list::link_lookup (generic_linked_list::with_generic_type::linked_list::link_lookup)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::with_generic_type::linked_list::link_lookup_copy (generic_linked_list::with_generic_type::linked_list::link_lookup_copy)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::with_generic_type::linked_list::link_len (generic_linked_list::with_generic_type::linked_list::link_len)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_list (generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_list)
[2023-09-08T21:37:05Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_peek (generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_peek)
[2023-09-08T21:37:06Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_peek_mut (generic_linked_list::with_generic_type::linked_list::prusti_tests::_test_peek_mut)
[2023-09-08T21:37:06Z INFO  prusti_viper::encoder::encoder] Encoding: generic_linked_list::with_generic_type::can_create_new (generic_linked_list::with_generic_type::can_create_new)
thread 'rustc' panicked at vir/src/../gen/high/operations_internal/expression.rs:288:13:
assertion `left == right` failed: _3 → m_with_generic_type$$linked_list$$link_lookup(_4, _6)
  left: Reference(Reference { lifetime: LifetimeConst { name: "lft_erased" }, uniqueness: Shared, target_type: Struct(Struct { name: "struct$m_with_generic_type$$range_generic$$Range", arguments: [TypeVar(GenericType(GenericType { name: "U$0" }))], lifetimes: [] }) })
 right: Reference(Reference { lifetime: LifetimeConst { name: "lft_erased" }, uniqueness: Shared, target_type: Struct(Struct { name: "struct$m_with_generic_type$$range_generic$$Range", arguments: [Struct(Struct { name: "struct$m_with_generic_type$$range_generic$$Range", arguments: [TypeVar(GenericType(GenericType { name: "U$0" }))], lifetimes: [] })], lifetimes: [] }) })
stack backtrace:
   0: rust_begin_unwind
             at /rustc/2f5df8a94bb3c5fae4e3fcbfc8ef20f1f976cb19/library/std/src/panicking.rs:619:5
   1: core::panicking::panic_fmt
             at /rustc/2f5df8a94bb3c5fae4e3fcbfc8ef20f1f976cb19/library/core/src/panicking.rs:72:14
   2: core::panicking::assert_failed_inner
   3: core::panicking::assert_failed
   4: vir::gen::high::operations_internal::expression::<impl vir::gen::high::ast::expression::Expression>::replace_place
   5: prusti_viper::encoder::mir::pure::interpreter::state_high::ExprBackwardInterpreterState::substitute_value
   6: prusti_viper::encoder::mir::pure::interpreter::interpreter_high::ExpressionBackwardInterpreter::encode_call_generic
   7: prusti_viper::encoder::mir::pure::interpreter::interpreter_high::ExpressionBackwardInterpreter::apply_call_terminator
   8: <prusti_viper::encoder::mir::pure::interpreter::interpreter_high::ExpressionBackwardInterpreter as prusti_viper::encoder::mir::pure::interpreter::backward_interpreter::BackwardMirInterpreter>::apply_terminator
   9: prusti_viper::encoder::mir::pure::interpreter::backward_interpreter::run_backward_interpretation
  10: prusti_viper::encoder::mir::pure::pure_functions::encoder_high::PureEncoder::encode_function_decl
  11: prusti_viper::encoder::mir::pure::pure_functions::encoder_high::encode_function_decl
  12: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::encode_pure_function_def::{{closure}}
  13: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::encode_pure_function_def
  14: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::ensure_pure_function_encoded
  15: prusti_viper::encoder::encoder::Encoder::get_function
  16: <prusti_viper::encoder::definition_collector::Collector as vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker>::fallible_walk_func_app
  17: vir::gen::polymorphic::ast::expr_transformers::default_fallible_walk_expr
  18: vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker::fallible_walk
  19: vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker::fallible_walk_bin_op
  20: vir::gen::polymorphic::ast::expr_transformers::default_fallible_walk_expr
  21: vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker::fallible_walk
  22: vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker::fallible_walk_bin_op
  23: vir::gen::polymorphic::ast::expr_transformers::default_fallible_walk_expr
  24: vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker::fallible_walk
  25: vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker::fallible_walk_bin_op
  26: vir::gen::polymorphic::ast::expr_transformers::default_fallible_walk_expr
  27: vir::gen::polymorphic::ast::expr_transformers::FallibleExprWalker::fallible_walk
  28: <prusti_viper::encoder::definition_collector::Collector as vir::gen::polymorphic::ast::stmt::FallibleStmtWalker>::fallible_walk_expr
  29: vir::gen::polymorphic::ast::stmt::FallibleStmtWalker::fallible_walk_inhale
  30: vir::gen::polymorphic::ast::stmt::FallibleStmtWalker::fallible_walk
  31: vir::gen::polymorphic::utils::fallible_walk_method::{{closure}}
  32: vir::gen::polymorphic::cfg::visitor::<impl vir::gen::polymorphic::cfg::method::CfgMethod>::fallible_walk_statements
  33: vir::gen::polymorphic::utils::fallible_walk_method
  34: vir::gen::polymorphic::utils::fallible_walk_methods
  35: prusti_viper::encoder::definition_collector::Collector::walk_methods
  36: prusti_viper::encoder::definition_collector::collect_definitions
  37: prusti_viper::encoder::encoder::Encoder::finalize_viper_program
  38: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
  39: prusti_viper::verifier::Verifier::verify
  40: prusti_driver::verifier::verify
  41: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis::{{closure}}
  42: rustc_middle::ty::context::GlobalCtxt::enter::{{closure}}
  43: rustc_middle::ty::context::tls::enter_context::{{closure}}
  44: std::thread::local::LocalKey<T>::try_with
  45: rustc_middle::ty::context::GlobalCtxt::enter
  46: rustc_interface::queries::QueryResult<&rustc_middle::ty::context::GlobalCtxt>::enter
  47: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis
  48: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

error: the compiler unexpectedly panicked. this is a bug.

note: we would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: please attach the file at `/home/ramla/Projects/generic_linked_list/rustc-ice-2023-09-08T21:37:05.072994371Z-440996.txt` to your bug report

note: compiler flags: --crate-type bin -C embed-bitcode=no -C debuginfo=2 -C incremental=[REDACTED]

note: some of the compiler flags provided by cargo are hidden

query stack during panic:
end of query stack
note: Prusti version: 0.2.2, commit 2258146 2023-09-06 16:44:48 UTC, built on 2023-09-06 16:53:05 UTC

[2023-09-08T21:37:06Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (1.149 seconds)
[2023-09-08T21:37:06Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (1.367 seconds)
error: could not compile `generic_linked_list` (bin "generic_linked_list") due to 2 previous errors; 2 warnings emitted

└──── End stderr ──────┘
Exit code 101, signal null.
Ignored diagnostic message: 'aborting due to previous error; 2 warnings emitted'
Rendering 1 diagnostics at file:///home/ramla/Projects/generic_linked_list/src/with_generic_type/range_generic.rs
Rendering 2 diagnostics at file:///home/ramla/Projects/generic_linked_list/src/with_generic_type/linked_list.rs
Ramla-I commented 1 year ago

rustc-ice-2023-09-08T21:37:05.072994371Z-440996.txt

vakaras commented 1 year ago

Could you try whether it helps to set use_new_encoder to false? At least for me, it fixes the problem on master.

We are in the process of refactoring Prusti and have a couple of checks that ensure that the results computed by the old and new code are the same. It seems that you found an example where this is not the case. Setting use_new_encoder to false disables the check.

Ramla-I commented 1 year ago

It fixes the problem for me too. Thanks for the solution!