Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Verifier won't detect trait functions for a usize wrapper type are pure #1409

Open
Ramla-I opened this issue Jun 6, 2023 · 0 comments
Open

Verifier won't detect trait functions for a usize wrapper type are pure #1409

Ramla-I opened this issue Jun 6, 2023 · 0 comments

Comments

@Ramla-I
Copy link

Ramla-I commented Jun 6, 2023

I'm having issues with implementing a wrapper type over a usize, I want to directly use the derived traits for Eq, Ord, etc. for this wrapper type. I ran all tests with the latest Prusti release version, and also had similar errors in the latest dev version.

One attempt used external specs to set those functions as pure so they can be used in the spec:

use prusti_contracts::*;

#[extern_spec]
impl Ord for usize {
    #[pure]
    fn cmp(&self, other: &Self) -> std::cmp::Ordering;
}


#[derive(Clone, Copy, Eq, PartialEq, PartialOrd, Ord)]
pub struct Frame(usize);

#[extern_spec]
impl PartialEq for Frame {
    #[pure]
    fn eq(&self, other: &Self) -> bool;

    #[pure]
    fn ne(&self, other: &Self) -> bool;
}

#[extern_spec]
impl Ord for Frame {
    #[pure]
    fn cmp(&self, other: &Self) -> std::cmp::Ordering ;
}

#[extern_spec]
impl PartialOrd for Frame {
    #[pure]
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering>;
}

fn main() {
    prusti_assert!(Frame(0) < Frame(1));
}

and here is the Prusti Assistant output:


Run verification on /home/ramla/Projects/prusti_test/src/main.rs...
Preparing verification run #3.
Killing 0 processes.
Run command '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/cargo-prusti --message-format=json'
Spawned PID: 905766
Output from '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/cargo-prusti --message-format=json' (0.2s):
┌──── Begin stdout ────┐
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.59 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/build/proc-macro2-ddffbdc041abc3ec/build-script-build"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"libc 0.2.145 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/build.rs","edition":"2015","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/build/libc-6fac23cbf046f5df/build-script-build"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"libc 0.2.145 (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/prusti_test/target/verify/debug/build/libc-da45cd2305e2e402/out"}
{"reason":"build-script-executed","package_id":"proc-macro2 1.0.59 (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/prusti_test/target/verify/debug/build/proc-macro2-4b2b9caffb58c252/out"}
{"reason":"compiler-artifact","package_id":"unicode-ident 1.0.9 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.9/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"unicode-ident","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.9/src/lib.rs","edition":"2018","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/prusti_test/target/verify/debug/deps/libunicode_ident-9ebdc1f9cef5775b.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libunicode_ident-9ebdc1f9cef5775b.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"quote 1.0.28 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/build/quote-7f289dad1b1bf6ef/build-script-build"],"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/github.com-1ecc6299db9ec823/syn-1.0.109/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/syn-1.0.109/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"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/prusti_test/target/verify/debug/build/syn-64ce62ad2ae3e70c/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/github.com-1ecc6299db9ec823/cfg-if-1.0.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"cfg-if","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/cfg-if-1.0.0/src/lib.rs","edition":"2018","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/prusti_test/target/verify/debug/deps/libcfg_if-90e3626e3c41eec3.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libcfg_if-90e3626e3c41eec3.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"either 1.8.1 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/either-1.8.1/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"either","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/either-1.8.1/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["use_std"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libeither-63a8f50ae3e85caa.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libeither-63a8f50ae3e85caa.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/github.com-1ecc6299db9ec823/rustc-hash-1.1.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"rustc-hash","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/rustc-hash-1.1.0/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","std"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/librustc_hash-91c665a5e97266ba.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/librustc_hash-91c665a5e97266ba.rmeta"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"quote 1.0.28 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":[],"env":[],"out_dir":"/home/ramla/Projects/prusti_test/target/verify/debug/build/quote-d5bb99a1e992c2f3/out"}
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.59 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"proc-macro2","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libproc_macro2-50e6efc6663fa681.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libproc_macro2-50e6efc6663fa681.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"libc 0.2.145 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"libc","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/src/lib.rs","edition":"2015","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/prusti_test/target/verify/debug/deps/liblibc-001399c14109dd2c.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/liblibc-001399c14109dd2c.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/prusti_test/target/verify/debug/build/syn-b9bc3cfc6eb142c3/out"}
{"reason":"compiler-artifact","package_id":"itertools 0.10.5 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/itertools-0.10.5/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"itertools","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/itertools-0.10.5/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","use_alloc","use_std"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libitertools-c8625afc49e04253.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libitertools-c8625afc49e04253.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"quote 1.0.28 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"quote","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libquote-26cc8377c792bd9f.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libquote-26cc8377c792bd9f.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"getrandom 0.2.9 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/getrandom-0.2.9/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"getrandom","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/getrandom-0.2.9/src/lib.rs","edition":"2018","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/prusti_test/target/verify/debug/deps/libgetrandom-01c2ea1549034c11.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libgetrandom-01c2ea1549034c11.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"uuid 1.3.3 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/uuid-1.3.3/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"uuid","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/uuid-1.3.3/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","getrandom","rng","std","v4"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libuuid-9556ce75da39b695.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libuuid-9556ce75da39b695.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/github.com-1ecc6299db9ec823/syn-1.0.109/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"syn","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/syn-1.0.109/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"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/prusti_test/target/verify/debug/deps/libsyn-77bf1faca38ecf05.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libsyn-77bf1faca38ecf05.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-specs 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-specs-0.1.7/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-specs","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-specs-0.1.7/src/lib.rs","edition":"2021","doc":true,"doctest":false,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libprusti_specs-c8e024e1adf21ce9.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libprusti_specs-c8e024e1adf21ce9.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts-proc-macros 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-proc-macros-0.1.6/Cargo.toml","target":{"kind":["proc-macro"],"crate_types":["proc-macro"],"name":"prusti-contracts-proc-macros","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-proc-macros-0.1.6/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/prusti_test/target/verify/debug/deps/libprusti_contracts_proc_macros-fe7ca5b74714c7b2.so"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts 0.1.4 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-0.1.4/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-contracts","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-0.1.4/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/prusti_test/target/verify/debug/deps/libprusti_contracts-d1c3b42fe68c16a8.rmeta"],"executable":null,"fresh":true}
{"reason":"build-finished","success":false}

└──── End stdout ──────┘
┌──── Begin stderr ────┐
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.565 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.657 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.124 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.511 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.569 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.045 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.334 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.094 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.923 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.921 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:44Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (2.122 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.375 seconds)
[2023-06-05T18:59:43Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.125 seconds)
[2023-06-05T18:59:43Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.387 seconds)
[2023-06-05T18:59:43Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:48Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (5.017 seconds)
[2023-06-05T18:59:46Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:48Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (2.293 seconds)
[2023-06-05T18:59:48Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:49Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.738 seconds)
[2023-06-05T19:11:30Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T19:11:30Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.052 seconds)
    Checking prusti_test v0.1.0 (/home/ramla/Projects/prusti_test)
[2023-06-06T19:12:08Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
thread 'rustc' panicked at 'internal error: entered unreachable code', prusti-interface/src/environment/query.rs:303:21
stack backtrace:
   0: rust_begin_unwind
             at /rustc/afaf3e07aaa7ca9873bdb439caec53faffa4230c/library/std/src/panicking.rs:575:5
   1: core::panicking::panic_fmt
             at /rustc/afaf3e07aaa7ca9873bdb439caec53faffa4230c/library/core/src/panicking.rs:64:14
   2: core::panicking::panic
             at /rustc/afaf3e07aaa7ca9873bdb439caec53faffa4230c/library/core/src/panicking.rs:114:5
   3: prusti_interface::environment::query::EnvQuery::find_impl_of_trait_method_call
   4: prusti_interface::specs::external::ExternSpecDeclaration::from_method_call
   5: prusti_interface::specs::external::ExternSpecResolver::add_extern_fn
   6: <prusti_interface::specs::SpecCollector as rustc_hir::intravisit::Visitor>::visit_fn
   7: rustc_hir::intravisit::walk_impl_item
   8: rustc_hir::intravisit::Visitor::visit_impl_item
   9: rustc_hir::intravisit::Visitor::visit_nested_impl_item
  10: rustc_hir::intravisit::walk_impl_item_ref
  11: rustc_hir::intravisit::Visitor::visit_impl_item_ref
  12: rustc_hir::intravisit::walk_item
  13: rustc_hir::intravisit::Visitor::visit_item
  14: rustc_hir::intravisit::Visitor::visit_nested_item
  15: rustc_hir::intravisit::walk_mod
  16: rustc_hir::intravisit::Visitor::visit_mod
  17: rustc_middle::hir::map::Map::walk_toplevel_module
  18: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis::{{closure}}
  19: rustc_interface::passes::QueryContext::enter::{{closure}}
  20: rustc_middle::ty::context::tls::enter_context::{{closure}}
  21: rustc_middle::ty::context::tls::set_tlv
  22: rustc_interface::passes::QueryContext::enter
  23: rustc_interface::queries::QueryResult<rustc_interface::passes::QueryContext>::enter
  24: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
  25: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
  26: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  27: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

error: internal compiler error: unexpected panic

note: Prusti or the compiler unexpectedly panicked. This is a bug.

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

note: Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC

query stack during panic:
end of query stack
[2023-06-06T19:12:08Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.077 seconds)
error: could not compile `prusti_test`

└──── End stderr ──────┘
Exit code 101, signal null.
Prusti encountered an unexpected error.
Prusti encountered an unexpected error. We would appreciate a [bug report](https://github.com/viperproject/prusti-dev/issues/new). See the log (View -> Output -> Prusti Assistant) for more details.

In another attempt I defined the traits myself:

use prusti_contracts::*;


#[extern_spec]
impl Ord for usize {
    #[pure]
    fn cmp(&self, other: &Self) -> std::cmp::Ordering;
}


#[derive(Clone, Copy, Eq)]
pub struct Frame(usize);

impl PartialEq for Frame {
    #[pure]
    fn eq(&self, other: &Self) -> bool {
        self.0 == other.0
    }

    #[pure]
    fn ne(&self, other: &Self) -> bool {
        self.0 != other.0
    }
}

impl Ord for Frame {
    #[pure]
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        self.0.cmp(&other.0)
    }
}

impl PartialOrd for Frame {
    #[pure]
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.cmp(other))
    }
}


fn main() {
    prusti_assert!(Frame(0) != Frame(1));
}

The prusti assistant output was:

Run verification on /home/ramla/Projects/prusti_test/src/main.rs...
Preparing verification run #7.
Killing 0 processes.
Run command '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/cargo-prusti --message-format=json'
Spawned PID: 906421
Output from '/home/ramla/.config/Code/User/globalStorage/viper-admin.prusti-assistant/prustiTools/LatestRelease/prusti/cargo-prusti --message-format=json' (0.4s):
┌──── Begin stdout ────┐
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.59 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/build/proc-macro2-ddffbdc041abc3ec/build-script-build"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"libc 0.2.145 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/build.rs","edition":"2015","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/build/libc-6fac23cbf046f5df/build-script-build"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"proc-macro2 1.0.59 (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/prusti_test/target/verify/debug/build/proc-macro2-4b2b9caffb58c252/out"}
{"reason":"compiler-artifact","package_id":"unicode-ident 1.0.9 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.9/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"unicode-ident","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.9/src/lib.rs","edition":"2018","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/prusti_test/target/verify/debug/deps/libunicode_ident-9ebdc1f9cef5775b.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libunicode_ident-9ebdc1f9cef5775b.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"quote 1.0.28 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/build/quote-7f289dad1b1bf6ef/build-script-build"],"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/github.com-1ecc6299db9ec823/syn-1.0.109/Cargo.toml","target":{"kind":["custom-build"],"crate_types":["bin"],"name":"build-script-build","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/syn-1.0.109/build.rs","edition":"2018","doc":false,"doctest":false,"test":false},"profile":{"opt_level":"0","debuginfo":2,"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/prusti_test/target/verify/debug/build/syn-64ce62ad2ae3e70c/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/github.com-1ecc6299db9ec823/cfg-if-1.0.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"cfg-if","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/cfg-if-1.0.0/src/lib.rs","edition":"2018","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/prusti_test/target/verify/debug/deps/libcfg_if-90e3626e3c41eec3.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libcfg_if-90e3626e3c41eec3.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"either 1.8.1 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/either-1.8.1/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"either","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/either-1.8.1/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["use_std"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libeither-63a8f50ae3e85caa.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libeither-63a8f50ae3e85caa.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/github.com-1ecc6299db9ec823/rustc-hash-1.1.0/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"rustc-hash","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/rustc-hash-1.1.0/src/lib.rs","edition":"2015","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","std"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/librustc_hash-91c665a5e97266ba.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/librustc_hash-91c665a5e97266ba.rmeta"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"libc 0.2.145 (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/prusti_test/target/verify/debug/build/libc-da45cd2305e2e402/out"}
{"reason":"compiler-artifact","package_id":"proc-macro2 1.0.59 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"proc-macro2","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/proc-macro2-1.0.59/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libproc_macro2-50e6efc6663fa681.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libproc_macro2-50e6efc6663fa681.rmeta"],"executable":null,"fresh":true}
{"reason":"build-script-executed","package_id":"quote 1.0.28 (registry+https://github.com/rust-lang/crates.io-index)","linked_libs":[],"linked_paths":[],"cfgs":[],"env":[],"out_dir":"/home/ramla/Projects/prusti_test/target/verify/debug/build/quote-d5bb99a1e992c2f3/out"}
{"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/prusti_test/target/verify/debug/build/syn-b9bc3cfc6eb142c3/out"}
{"reason":"compiler-artifact","package_id":"itertools 0.10.5 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/itertools-0.10.5/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"itertools","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/itertools-0.10.5/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":false},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","use_alloc","use_std"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libitertools-c8625afc49e04253.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libitertools-c8625afc49e04253.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"libc 0.2.145 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"libc","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/libc-0.2.145/src/lib.rs","edition":"2015","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/prusti_test/target/verify/debug/deps/liblibc-001399c14109dd2c.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/liblibc-001399c14109dd2c.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"quote 1.0.28 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"quote","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/quote-1.0.28/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","proc-macro"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libquote-26cc8377c792bd9f.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libquote-26cc8377c792bd9f.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"getrandom 0.2.9 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/getrandom-0.2.9/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"getrandom","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/getrandom-0.2.9/src/lib.rs","edition":"2018","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/prusti_test/target/verify/debug/deps/libgetrandom-01c2ea1549034c11.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libgetrandom-01c2ea1549034c11.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/github.com-1ecc6299db9ec823/syn-1.0.109/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"syn","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/syn-1.0.109/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"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/prusti_test/target/verify/debug/deps/libsyn-77bf1faca38ecf05.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libsyn-77bf1faca38ecf05.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"uuid 1.3.3 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/uuid-1.3.3/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"uuid","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/uuid-1.3.3/src/lib.rs","edition":"2018","doc":true,"doctest":true,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":["default","getrandom","rng","std","v4"],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libuuid-9556ce75da39b695.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libuuid-9556ce75da39b695.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-specs 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-specs-0.1.7/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-specs","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-specs-0.1.7/src/lib.rs","edition":"2021","doc":true,"doctest":false,"test":true},"profile":{"opt_level":"0","debuginfo":2,"debug_assertions":true,"overflow_checks":true,"test":false},"features":[],"filenames":["/home/ramla/Projects/prusti_test/target/verify/debug/deps/libprusti_specs-c8e024e1adf21ce9.rlib","/home/ramla/Projects/prusti_test/target/verify/debug/deps/libprusti_specs-c8e024e1adf21ce9.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts-proc-macros 0.1.6 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-proc-macros-0.1.6/Cargo.toml","target":{"kind":["proc-macro"],"crate_types":["proc-macro"],"name":"prusti-contracts-proc-macros","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-proc-macros-0.1.6/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/prusti_test/target/verify/debug/deps/libprusti_contracts_proc_macros-fe7ca5b74714c7b2.so"],"executable":null,"fresh":true}
{"reason":"compiler-artifact","package_id":"prusti-contracts 0.1.4 (registry+https://github.com/rust-lang/crates.io-index)","manifest_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-0.1.4/Cargo.toml","target":{"kind":["lib"],"crate_types":["lib"],"name":"prusti-contracts","src_path":"/home/ramla/.cargo/registry/src/github.com-1ecc6299db9ec823/prusti-contracts-0.1.4/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/prusti_test/target/verify/debug/deps/libprusti_contracts-d1c3b42fe68c16a8.rmeta"],"executable":null,"fresh":true}
{"reason":"compiler-message","package_id":"prusti_test 0.1.0 (path+file:///home/ramla/Projects/prusti_test)","manifest_path":"/home/ramla/Projects/prusti_test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test","src_path":"/home/ramla/Projects/prusti_test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"error: [Prusti: unsupported feature] unsupported constant type Ref(ReErased, Frame, Not)\n  --> src/main.rs:43:32\n   |\n43 |     prusti_assert!(Frame(0) != Frame(1));\n   |                                ^^^^^^^^\n\n","children":[],"code":null,"level":"error","message":"[Prusti: unsupported feature] unsupported constant type Ref(ReErased, Frame, Not)","spans":[{"byte_end":765,"byte_start":757,"column_end":40,"column_start":32,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":43,"line_start":43,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":40,"highlight_start":32,"text":"    prusti_assert!(Frame(0) != Frame(1));"}]}]}}
{"reason":"compiler-message","package_id":"prusti_test 0.1.0 (path+file:///home/ramla/Projects/prusti_test)","manifest_path":"/home/ramla/Projects/prusti_test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test","src_path":"/home/ramla/Projects/prusti_test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"error: [Prusti: invalid specification] use of impure function \"std::cmp::Ord::cmp\" in pure code is not allowed\n  --> src/main.rs:30:9\n   |\n30 |         self.0.cmp(&other.0)\n   |         ^^^^^^^^^^^^^^^^^^^^\n\n","children":[],"code":null,"level":"error","message":"[Prusti: invalid specification] use of impure function \"std::cmp::Ord::cmp\" in pure code is not allowed","spans":[{"byte_end":552,"byte_start":532,"column_end":29,"column_start":9,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":30,"line_start":30,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":29,"highlight_start":9,"text":"        self.0.cmp(&other.0)"}]}]}}
{"reason":"compiler-message","package_id":"prusti_test 0.1.0 (path+file:///home/ramla/Projects/prusti_test)","manifest_path":"/home/ramla/Projects/prusti_test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test","src_path":"/home/ramla/Projects/prusti_test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"error: [Prusti: invalid specification] use of impure function \"std::cmp::Ord::cmp\" in pure code is not allowed\n  --> src/main.rs:37:14\n   |\n37 |         Some(self.cmp(other))\n   |              ^^^^^^^^^^^^^^^\n\n","children":[],"code":null,"level":"error","message":"[Prusti: invalid specification] use of impure function \"std::cmp::Ord::cmp\" in pure code is not allowed","spans":[{"byte_end":702,"byte_start":687,"column_end":29,"column_start":14,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":37,"line_start":37,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":29,"highlight_start":14,"text":"        Some(self.cmp(other))"}]}]}}
{"reason":"compiler-message","package_id":"prusti_test 0.1.0 (path+file:///home/ramla/Projects/prusti_test)","manifest_path":"/home/ramla/Projects/prusti_test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test","src_path":"/home/ramla/Projects/prusti_test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"error: [Prusti: verification error] precondition of pure function call might not hold.\n  --> src/main.rs:37:14\n   |\n37 |         Some(self.cmp(other))\n   |              ^^^^^^^^^^^^^^^\n\n","children":[],"code":null,"level":"error","message":"[Prusti: verification error] precondition of pure function call might not hold.","spans":[{"byte_end":702,"byte_start":687,"column_end":29,"column_start":14,"expansion":null,"file_name":"src/main.rs","is_primary":true,"label":null,"line_end":37,"line_start":37,"suggested_replacement":null,"suggestion_applicability":null,"text":[{"highlight_end":29,"highlight_start":14,"text":"        Some(self.cmp(other))"}]}]}}
{"reason":"compiler-message","package_id":"prusti_test 0.1.0 (path+file:///home/ramla/Projects/prusti_test)","manifest_path":"/home/ramla/Projects/prusti_test/Cargo.toml","target":{"kind":["bin"],"crate_types":["bin"],"name":"prusti_test","src_path":"/home/ramla/Projects/prusti_test/src/main.rs","edition":"2021","doc":true,"doctest":false,"test":true},"message":{"rendered":"error: aborting due to 4 previous errors\n\n","children":[],"code":null,"level":"error","message":"aborting due to 4 previous errors","spans":[]}}
{"reason":"build-finished","success":false}

└──── End stdout ──────┘
┌──── Begin stderr ────┐
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.565 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.657 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.124 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.511 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:42Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.569 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.045 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.334 seconds)
[2023-06-05T18:59:41Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:41Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.094 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.923 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:44Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (2.122 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.921 seconds)
[2023-06-05T18:59:42Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.375 seconds)
[2023-06-05T18:59:43Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.125 seconds)
[2023-06-05T18:59:43Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:48Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (5.017 seconds)
[2023-06-05T18:59:43Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:43Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.387 seconds)
[2023-06-05T18:59:46Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:48Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (2.293 seconds)
[2023-06-05T18:59:48Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T18:59:49Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.738 seconds)
[2023-06-05T19:11:30Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-05T19:11:30Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.052 seconds)
    Checking prusti_test v0.1.0 (/home/ramla/Projects/prusti_test)
[2023-06-06T19:20:19Z INFO  prusti_driver] Prusti version: 0.2.1, commit 706512a 2023-01-26 17:24:53 UTC, built on 2023-01-26 17:35:07 UTC
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier] Received 7 functions to be verified:
[2023-06-06T19:20:19Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Starting: encoding to Viper
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]  - main (prusti_test::main)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]    Source: src/main.rs:42:1: 42:10 (#0)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]  - <Frame as std::clone::Clone>::clone (prusti_test::{impl#4}::clone)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]    Source: src/main.rs:12:10: 12:15 (#8)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]  - <Frame as std::cmp::Eq>::assert_receiver_is_total_eq (prusti_test::{impl#7}::assert_receiver_is_total_eq)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]    Source: src/main.rs:12:23: 12:25 (#10)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]  - <Frame as std::cmp::PartialEq>::eq (prusti_test::{impl#0}::eq)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]    Source: src/main.rs:17:5: 17:39 (#0)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]  - <Frame as std::cmp::PartialEq>::ne (prusti_test::{impl#0}::ne)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]    Source: src/main.rs:22:5: 22:39 (#0)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]  - <Frame as std::cmp::Ord>::cmp (prusti_test::{impl#1}::cmp)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]    Source: src/main.rs:29:5: 29:54 (#0)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]  - <Frame as std::cmp::PartialOrd>::partial_cmp (prusti_test::{impl#2}::partial_cmp)
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier]    Source: src/main.rs:36:5: 36:70 (#0)
[2023-06-06T19:20:19Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_test::main (prusti_test::main)
[2023-06-06T19:20:19Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_test::<Frame as std::clone::Clone>::clone (prusti_test::{impl#4}::clone)
[2023-06-06T19:20:19Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_test::<Frame as std::cmp::Eq>::assert_receiver_is_total_eq (prusti_test::{impl#7}::assert_receiver_is_total_eq)
[2023-06-06T19:20:19Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_test::<Frame as std::cmp::PartialEq>::eq (prusti_test::{impl#0}::eq)
[2023-06-06T19:20:19Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_test::<Frame as std::cmp::PartialEq>::ne (prusti_test::{impl#0}::ne)
[2023-06-06T19:20:19Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_test::<Frame as std::cmp::Ord>::cmp (prusti_test::{impl#1}::cmp)
[2023-06-06T19:20:19Z INFO  prusti_viper::encoder::encoder] Encoding: prusti_test::<Frame as std::cmp::PartialOrd>::partial_cmp (prusti_test::{impl#2}::partial_cmp)
[2023-06-06T19:20:19Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Completed: encoding to Viper (0.076 seconds)
[2023-06-06T19:20:19Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Starting: optimizing Viper program
[2023-06-06T19:20:19Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Completed: optimizing Viper program (0.010 seconds)
[2023-06-06T19:20:19Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Starting: verifying Viper program
[2023-06-06T19:20:19Z INFO  prusti_viper::verifier] Connecting to Prusti server at localhost:45229
[2023-06-06T19:20:19Z INFO  prusti_utils::stopwatch::log_level] [prusti-viper] Completed: verifying Viper program (0.010 seconds)
[2023-06-06T19:20:19Z INFO  prusti_utils::stopwatch::log_level] [prusti] Completed: main (0.152 seconds)
error: could not compile `prusti_test` due to 5 previous errors

└──── End stderr ──────┘
Exit code 101, signal null.
Ignored diagnostic message: 'aborting due to 4 previous errors'
Rendering 4 diagnostics at file:///home/ramla/Projects/prusti_test/src/main.rs

and prusti server output was:

 [stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Verification request hash: 5906111797969873958 - for program main.rs_prusti_test::main
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Using cached result Success for program main.rs_prusti_test::main
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Verification request hash: 14590329135090302195 - for program main.rs_prusti_test::<Frame as std::clone::Clone>::clone
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Using cached result Success for program main.rs_prusti_test::<Frame as std::clone::Clone>::clone
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Verification request hash: 16311625901828985734 - for program main.rs_prusti_test::<Frame as std::cmp::Eq>::assert_receiver_is_total_eq
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Using cached result Success for program main.rs_prusti_test::<Frame as std::cmp::Eq>::assert_receiver_is_total_eq
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[stderr] [2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Verification request hash: 5824969992159800103 - for program main.rs_prusti_test::<Frame as std::cmp::PartialEq>::eq
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Using cached result Success for program main.rs_prusti_test::<Frame as std::cmp::PartialEq>::eq
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Verification request hash: 7508710382242282684 - for program main.rs_prusti_test::<Frame as std::cmp::PartialEq>::ne
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Using cached result Success for program main.rs_prusti_test::<Frame as std::cmp::PartialEq>::ne
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[stderr] [2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Verification request hash: 13034001164752554546 - for program main.rs_prusti_test::<Frame as std::cmp::Ord>::cmp
[2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Using cached result Success for program main.rs_prusti_test::<Frame as std::cmp::Ord>::cmp
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Starting: attach thread to JVM
[stderr] [2023-06-06T19:20:49Z INFO  prusti_utils::stopwatch::log_level] [prusti-server] Completed: attach thread to JVM (0.000 seconds)
[stderr] [2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Verification request hash: 1413869375259229944 - for program main.rs_prusti_test::<Frame as std::cmp::PartialOrd>::partial_cmp
[stderr] [2023-06-06T19:20:49Z INFO  prusti_server::process_verification] Using cached result Failure([VerificationError { full_id: "application.precondition:assertion.false", pos_id: Some("4"), offending_pos_id: Some("4"), reason_pos_id: Some("0"), message: "Precondition of function m_$openang$Frame$space$as$space$std$$cmp$$Ord$closeang$$$cmp__$TY$__Snap$struct$m_Frame$Snap$struct$m_Frame$Snap$m_std$$cmp$$Ordering$_beg_$_end_ might not hold. Assertion false might not hold. (@45.14)\n", counterexample: None }]) for program main.rs_prusti_test::<Frame as std::cmp::PartialOrd>::partial_cmp

I don't see why the verifier refuses to identify a trait function as pure when I've marked it as so.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@Ramla-I