[INFO] fetching crate vstd 0.0.0-2026-04-12-0118... [INFO] testing vstd-0.0.0-2026-04-12-0118 against master#562dee4820c458d823175268e41601d4c060588a for pr-154210-2 [INFO] extracting crate vstd 0.0.0-2026-04-12-0118 into /workspace/builds/worker-7-tc1/source [INFO] started tweaking crates.io crate vstd 0.0.0-2026-04-12-0118 [INFO] finished tweaking crates.io crate vstd 0.0.0-2026-04-12-0118 [INFO] tweaked toml for crates.io crate vstd 0.0.0-2026-04-12-0118 written to /workspace/builds/worker-7-tc1/source/Cargo.toml [INFO] validating manifest of crates.io crate vstd 0.0.0-2026-04-12-0118 on toolchain 562dee4820c458d823175268e41601d4c060588a [INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+562dee4820c458d823175268e41601d4c060588a" "metadata" "--manifest-path" "Cargo.toml" "--no-deps", kill_on_drop: false }` [INFO] crate crates.io crate vstd 0.0.0-2026-04-12-0118 already has a lockfile, it will not be regenerated [INFO] running `Command { std: CARGO_HOME="/workspace/cargo-home" RUSTUP_HOME="/workspace/rustup-home" "/workspace/cargo-home/bin/cargo" "+562dee4820c458d823175268e41601d4c060588a" "fetch" "--manifest-path" "Cargo.toml", kill_on_drop: false }` [INFO] [stderr] Updating crates.io index [INFO] [stderr] Downloading crates ... [INFO] [stderr] Downloaded verus_builtin v0.0.0-2026-04-12-0118 [INFO] [stderr] Downloaded verus_builtin_macros v0.0.0-2026-04-12-0118 [INFO] [stderr] Downloaded verus_prettyplease v0.0.0-2026-04-12-0118 [INFO] [stderr] Downloaded verus_syn v0.0.0-2026-04-05-0114 [INFO] [stderr] Downloaded verus_state_machines_macros v0.0.0-2026-04-05-0114 [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+562dee4820c458d823175268e41601d4c060588a" "metadata" "--no-deps" "--format-version=1", kill_on_drop: false }` [INFO] [stdout] 374ac14273737eb2b066fcfceacc6e426ec650b1ebba953aeb516bd127e9b909 [INFO] running `Command { std: "docker" "start" "-a" "374ac14273737eb2b066fcfceacc6e426ec650b1ebba953aeb516bd127e9b909", kill_on_drop: false }` [INFO] running `Command { std: "docker" "inspect" "374ac14273737eb2b066fcfceacc6e426ec650b1ebba953aeb516bd127e9b909", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "374ac14273737eb2b066fcfceacc6e426ec650b1ebba953aeb516bd127e9b909", kill_on_drop: false }` [INFO] [stdout] 374ac14273737eb2b066fcfceacc6e426ec650b1ebba953aeb516bd127e9b909 [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=forbid" "-e" "RUSTDOCFLAGS=--cap-lints=forbid" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+562dee4820c458d823175268e41601d4c060588a" "build" "--frozen" "--message-format=json", kill_on_drop: false }` [INFO] [stdout] fc89f473f72ef8629b717d4fee4d8ab9e8d93b5c6cb7766d2850f8a3454df04c [INFO] running `Command { std: "docker" "start" "-a" "fc89f473f72ef8629b717d4fee4d8ab9e8d93b5c6cb7766d2850f8a3454df04c", kill_on_drop: false }` [INFO] [stderr] Compiling proc-macro2 v1.0.106 [INFO] [stderr] Compiling verus_prettyplease v0.0.0-2026-04-12-0118 [INFO] [stderr] Compiling hashbrown v0.12.3 [INFO] [stderr] Compiling vstd v0.0.0-2026-04-12-0118 (/opt/rustwide/workdir) [INFO] [stderr] Compiling verus_builtin v0.0.0-2026-04-12-0118 [INFO] [stderr] Compiling indexmap v1.9.3 [INFO] [stderr] Compiling quote v1.0.45 [INFO] [stderr] Compiling verus_syn v0.0.0-2026-04-05-0114 [INFO] [stderr] Compiling syn v2.0.117 [INFO] [stderr] Compiling synstructure v0.13.2 [INFO] [stderr] Compiling verus_state_machines_macros v0.0.0-2026-04-05-0114 [INFO] [stderr] Compiling verus_builtin_macros v0.0.0-2026-04-12-0118 [INFO] [stdout] warning: unused variable: `future` [INFO] [stdout] --> future.rs:33:26 [INFO] [stdout] | [INFO] [stdout] 33 | fn exec_await(future: F) -> (ret: F::Output) [INFO] [stdout] | ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future` [INFO] [stdout] | [INFO] [stdout] = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default [INFO] [stdout] [INFO] [stdout] [INFO] [stderr] Finished `dev` profile [unoptimized + debuginfo] target(s) in 33.59s [INFO] running `Command { std: "docker" "inspect" "fc89f473f72ef8629b717d4fee4d8ab9e8d93b5c6cb7766d2850f8a3454df04c", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "fc89f473f72ef8629b717d4fee4d8ab9e8d93b5c6cb7766d2850f8a3454df04c", kill_on_drop: false }` [INFO] [stdout] fc89f473f72ef8629b717d4fee4d8ab9e8d93b5c6cb7766d2850f8a3454df04c [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=forbid" "-e" "RUSTDOCFLAGS=--cap-lints=forbid" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+562dee4820c458d823175268e41601d4c060588a" "test" "--frozen" "--no-run" "--message-format=json", kill_on_drop: false }` [INFO] [stdout] e994e9c9f9449265525e8758e01b168d2f246b39cd9989415327a4710ec2de54 [INFO] running `Command { std: "docker" "start" "-a" "e994e9c9f9449265525e8758e01b168d2f246b39cd9989415327a4710ec2de54", kill_on_drop: false }` [INFO] [stderr] Compiling vstd v0.0.0-2026-04-12-0118 (/opt/rustwide/workdir) [INFO] [stdout] warning: unused variable: `future` [INFO] [stdout] --> future.rs:33:26 [INFO] [stdout] | [INFO] [stdout] 33 | fn exec_await(future: F) -> (ret: F::Output) [INFO] [stdout] | ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future` [INFO] [stdout] | [INFO] [stdout] = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default [INFO] [stdout] [INFO] [stdout] [INFO] [stdout] warning: unused variable: `future` [INFO] [stdout] --> future.rs:33:26 [INFO] [stdout] | [INFO] [stdout] 33 | fn exec_await(future: F) -> (ret: F::Output) [INFO] [stdout] | ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future` [INFO] [stdout] | [INFO] [stdout] = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default [INFO] [stdout] [INFO] [stdout] [INFO] [stderr] Finished `test` profile [unoptimized + debuginfo] target(s) in 4.01s [INFO] running `Command { std: "docker" "inspect" "e994e9c9f9449265525e8758e01b168d2f246b39cd9989415327a4710ec2de54", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "e994e9c9f9449265525e8758e01b168d2f246b39cd9989415327a4710ec2de54", kill_on_drop: false }` [INFO] [stdout] e994e9c9f9449265525e8758e01b168d2f246b39cd9989415327a4710ec2de54 [INFO] running `Command { std: "docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-7-tc1/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=forbid" "-e" "RUSTDOCFLAGS=--cap-lints=forbid" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--user" "0:0" "--network" "none" "ghcr.io/rust-lang/crates-build-env/linux@sha256:d429b63d4308055ea97f60fb1d3dfca48854a00942f1bd2ad806beaf015945ec" "/opt/rustwide/cargo-home/bin/cargo" "+562dee4820c458d823175268e41601d4c060588a" "test" "--frozen", kill_on_drop: false }` [INFO] [stdout] 3ecafc2e3cf68d3c97bd89991b79e0678049b3c1f7dd8ce535d72ef360036e76 [INFO] running `Command { std: "docker" "start" "-a" "3ecafc2e3cf68d3c97bd89991b79e0678049b3c1f7dd8ce535d72ef360036e76", kill_on_drop: false }` [INFO] [stderr] warning: unused variable: `future` [INFO] [stderr] --> future.rs:33:26 [INFO] [stderr] | [INFO] [stderr] 33 | fn exec_await(future: F) -> (ret: F::Output) [INFO] [stderr] | ^^^^^^ help: if this is intentional, prefix it with an underscore: `_future` [INFO] [stderr] | [INFO] [stderr] = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default [INFO] [stderr] [INFO] [stderr] warning: `vstd` (lib) generated 1 warning (run `cargo fix --lib -p vstd` to apply 1 suggestion) [INFO] [stderr] warning: `vstd` (lib test) generated 1 warning (1 duplicate) [INFO] [stderr] Finished `test` profile [unoptimized + debuginfo] target(s) in 0.05s [INFO] [stderr] Running unittests vstd.rs (/opt/rustwide/target/debug/deps/vstd-7d8d799f50562f31) [INFO] [stdout] [INFO] [stdout] running 0 tests [INFO] [stdout] [INFO] [stdout] test result: ok. 0 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 0.00s [INFO] [stdout] [INFO] [stderr] Doc-tests vstd [INFO] [stdout] [INFO] [stdout] running 36 tests [INFO] [stdout] test cell/invcell.rs - cell::invcell::InvCell (line 23) ... ignored [INFO] [stdout] test cell/invcell.rs - cell::invcell::InvCell (line 45) ... ignored [INFO] [stdout] test cell/pcell.rs - cell::pcell::PCell (line 55) ... ignored [INFO] [stdout] test cell/pcell_maybe_uninit.rs - cell::pcell_maybe_uninit::PCell (line 21) ... ignored [INFO] [stdout] test atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 299) ... FAILED [INFO] [stdout] test arithmetic/overflow.rs - arithmetic::overflow (line 13) ... FAILED [INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 483) ... FAILED [INFO] [stdout] test invariant.rs - invariant::open_atomic_invariant (line 355) ... FAILED [INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 462) ... FAILED [INFO] [stdout] test map.rs - map::assert_maps_equal (line 355) ... FAILED [INFO] [stdout] test map.rs - map::assert_maps_equal (line 368) ... FAILED [INFO] [stdout] test atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 230) ... FAILED [INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 499) ... FAILED [INFO] [stdout] test rwlock.rs - rwlock::RwLock (line 278) ... ignored [INFO] [stdout] test rwlock.rs - rwlock::RwLock (line 309) ... ignored [INFO] [stdout] test calc_macro.rs - calc_macro::calc (line 37) ... FAILED [INFO] [stdout] test pervasive.rs - pervasive::assert_by_contradiction (line 225) ... FAILED [INFO] [stdout] test seq_lib.rs - seq_lib::assert_seqs_equal (line 3576) ... FAILED [INFO] [stdout] test calc_macro.rs - calc_macro::calc (line 17) ... FAILED [INFO] [stdout] test invariant.rs - invariant::open_local_invariant (line 508) ... FAILED [INFO] [stdout] test seq_lib.rs - seq_lib::assert_seqs_equal (line 3557) ... FAILED [INFO] [stdout] test raw_ptr.rs - raw_ptr::PointsTo (line 110) ... ok [INFO] [stdout] test pervasive.rs - pervasive::struct_with_invariants (line 306) ... FAILED [INFO] [stdout] test thread.rs - thread::spawn (line 68) ... ignored [INFO] [stdout] test set_lib.rs - set_lib::assert_sets_equal (line 1511) ... FAILED [INFO] [stdout] test tokens/frac.rs - tokens::frac::FracGhost (line 86) ... FAILED [INFO] [stdout] test pervasive.rs - pervasive::struct_with_invariants (line 276) ... FAILED [INFO] [stdout] test set_lib.rs - set_lib::assert_sets_equal (line 1505) ... FAILED [INFO] [stdout] test simple_pptr.rs - simple_pptr::PPtr (line 118) ... FAILED [INFO] [stdout] test seq.rs - seq::seq (line 541) ... FAILED [INFO] [stdout] test tokens/map.rs - tokens::map (line 19) ... FAILED [INFO] [stdout] test tokens/frac.rs - tokens::frac::GhostVarAuth (line 335) ... FAILED [INFO] [stdout] test simple_pptr.rs - simple_pptr::PPtr (line 92) ... FAILED [INFO] [stdout] test simple_pptr.rs - simple_pptr::PPtr (line 58) ... FAILED [INFO] [stdout] test tokens/seq.rs - tokens::seq::GhostSeqAuth (line 23) ... FAILED [INFO] [stdout] test tokens/set.rs - tokens::set (line 20) ... FAILED [INFO] [stdout] [INFO] [stdout] failures: [INFO] [stdout] [INFO] [stdout] ---- atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 299) stdout ---- [INFO] [stdout] error: cannot find macro `atomic_with_ghost` in this scope [INFO] [stdout] --> atomic_ghost.rs:300:14 [INFO] [stdout] | [INFO] [stdout] 300 | let result = atomic_with_ghost!( [INFO] [stdout] | ^^^^^^^^^^^^^^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 299 + use vstd::atomic_with_ghost; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- arithmetic/overflow.rs - arithmetic::overflow (line 13) stdout ---- [INFO] [stdout] error: expected one of `!`, `(`, `)`, `+`, `,`, `::`, or `<`, found `:` [INFO] [stdout] --> arithmetic/overflow.rs:27:47 [INFO] [stdout] | [INFO] [stdout] 27 | fn test2(a: u64, b: u64, c: u64, d: u64) -> (e: Option) [INFO] [stdout] | ^ expected one of 7 possible tokens [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 483) stdout ---- [INFO] [stdout] error: expected pattern, found `$` [INFO] [stdout] --> invariant.rs:485:9 [INFO] [stdout] | [INFO] [stdout] 485 | let $id: V = /* an arbitrary value */; [INFO] [stdout] | ^ expected pattern [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- invariant.rs - invariant::open_atomic_invariant (line 355) stdout ---- [INFO] [stdout] error: expected expression, found `$` [INFO] [stdout] --> invariant.rs:356:23 [INFO] [stdout] | [INFO] [stdout] 356 | open_atomic_invariant($inv => $id => { [INFO] [stdout] | ^ expected expression [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 462) stdout ---- [INFO] [stdout] error: expected expression, found `$` [INFO] [stdout] --> invariant.rs:463:22 [INFO] [stdout] | [INFO] [stdout] 463 | open_local_invariant($inv => $id => { [INFO] [stdout] | ^ expected expression [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- map.rs - map::assert_maps_equal (line 355) stdout ---- [INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn` [INFO] [stdout] --> map.rs:356:7 [INFO] [stdout] | [INFO] [stdout] 356 | proof fn insert_remove(m: Map, k: int, v: int) [INFO] [stdout] | ^^ expected one of `!` or `::` [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- map.rs - map::assert_maps_equal (line 368) stdout ---- [INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn` [INFO] [stdout] --> map.rs:369:7 [INFO] [stdout] | [INFO] [stdout] 369 | proof fn bitvector_maps() { [INFO] [stdout] | ^^ expected one of `!` or `::` [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 230) stdout ---- [INFO] [stdout] error: cannot find macro `atomic_with_ghost` in this scope [INFO] [stdout] --> atomic_ghost.rs:231:14 [INFO] [stdout] | [INFO] [stdout] 231 | let result = atomic_with_ghost!( [INFO] [stdout] | ^^^^^^^^^^^^^^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 230 + use vstd::atomic_with_ghost; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 499) stdout ---- [INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `=>` [INFO] [stdout] --> invariant.rs:500:26 [INFO] [stdout] | [INFO] [stdout] 500 | open_local_invariant(inv => id1 => { [INFO] [stdout] | ^^ expected one of 8 possible tokens [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- calc_macro.rs - calc_macro::calc (line 37) stdout ---- [INFO] [stdout] error: cannot find macro `calc` in this scope [INFO] [stdout] --> calc_macro.rs:40:1 [INFO] [stdout] | [INFO] [stdout] 40 | calc! { [INFO] [stdout] | ^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 37 + use vstd::calc; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find type `int` in this scope [INFO] [stdout] --> calc_macro.rs:38:8 [INFO] [stdout] | [INFO] [stdout] 38 | let x: int = 2; [INFO] [stdout] | ^^^ not found in this scope [INFO] [stdout] | [INFO] [stdout] help: perhaps you intended to use this type [INFO] [stdout] | [INFO] [stdout] 38 - let x: int = 2; [INFO] [stdout] 38 + let x: i32 = 2; [INFO] [stdout] | [INFO] [stdout] help: consider importing one of these structs [INFO] [stdout] | [INFO] [stdout] 37 + use verus_builtin::int; [INFO] [stdout] | [INFO] [stdout] 37 + use vstd::prelude::int; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find type `int` in this scope [INFO] [stdout] --> calc_macro.rs:39:8 [INFO] [stdout] | [INFO] [stdout] 39 | let y: int = 5; [INFO] [stdout] | ^^^ not found in this scope [INFO] [stdout] | [INFO] [stdout] help: perhaps you intended to use this type [INFO] [stdout] | [INFO] [stdout] 39 - let y: int = 5; [INFO] [stdout] 39 + let y: i32 = 5; [INFO] [stdout] | [INFO] [stdout] help: consider importing one of these structs [INFO] [stdout] | [INFO] [stdout] 37 + use verus_builtin::int; [INFO] [stdout] | [INFO] [stdout] 37 + use vstd::prelude::int; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 3 previous errors [INFO] [stdout] [INFO] [stdout] For more information about this error, try `rustc --explain E0425`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- pervasive.rs - pervasive::assert_by_contradiction (line 225) stdout ---- [INFO] [stdout] error: cannot find macro `assert_by_contradiction` in this scope [INFO] [stdout] --> pervasive.rs:226:1 [INFO] [stdout] | [INFO] [stdout] 226 | assert_by_contradiction!(b, { [INFO] [stdout] | ^^^^^^^^^^^^^^^^^^^^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 225 + use vstd::assert_by_contradiction; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- seq_lib.rs - seq_lib::assert_seqs_equal (line 3576) stdout ---- [INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn` [INFO] [stdout] --> seq_lib.rs:3577:7 [INFO] [stdout] | [INFO] [stdout] 3577 | proof fn bitvector_seqs() { [INFO] [stdout] | ^^ expected one of `!` or `::` [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- calc_macro.rs - calc_macro::calc (line 17) stdout ---- [INFO] [stdout] error: cannot find macro `calc` in this scope [INFO] [stdout] --> calc_macro.rs:18:1 [INFO] [stdout] | [INFO] [stdout] 18 | calc! { [INFO] [stdout] | ^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 17 + use vstd::calc; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- invariant.rs - invariant::open_local_invariant (line 508) stdout ---- [INFO] [stdout] error: mismatched closing delimiter: `}` [INFO] [stdout] --> invariant.rs:513:32 [INFO] [stdout] | [INFO] [stdout] 511 | | open_local_invariant!(&inv => id1 => { [INFO] [stdout] | - closing delimiter possibly meant for this [INFO] [stdout] 512 | | ^ this invariant [INFO] [stdout] 513 | | open_local_invariant!(&inv => id2 => { [INFO] [stdout] | ^ unclosed delimiter [INFO] [stdout] ... [INFO] [stdout] 517 | | } [INFO] [stdout] | ^ mismatched closing delimiter [INFO] [stdout] [INFO] [stdout] error: this file contains an unclosed delimiter [INFO] [stdout] --> invariant.rs:517:8 [INFO] [stdout] | [INFO] [stdout] 511 | | open_local_invariant!(&inv => id1 => { [INFO] [stdout] | - unclosed delimiter [INFO] [stdout] ... [INFO] [stdout] 517 | | } [INFO] [stdout] | ^ [INFO] [stdout] [INFO] [stdout] error: aborting due to 2 previous errors [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- seq_lib.rs - seq_lib::assert_seqs_equal (line 3557) stdout ---- [INFO] [stdout] error: expected one of `!` or `::`, found keyword `fn` [INFO] [stdout] --> seq_lib.rs:3558:7 [INFO] [stdout] | [INFO] [stdout] 3558 | proof fn subrange_concat(s: Seq, i: int) { [INFO] [stdout] | ^^ expected one of `!` or `::` [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- pervasive.rs - pervasive::struct_with_invariants (line 306) stdout ---- [INFO] [stdout] error: expected one of `!` or `::`, found `:` [INFO] [stdout] --> pervasive.rs:307:20 [INFO] [stdout] | [INFO] [stdout] 307 | BoolPredicateDecl := predicate { $bool_expr } [INFO] [stdout] | ^ expected one of `!` or `::` [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- set_lib.rs - set_lib::assert_sets_equal (line 1511) stdout ---- [INFO] [stdout] error: cannot find macro `assert_sets_equal` in this scope [INFO] [stdout] --> set_lib.rs:1512:1 [INFO] [stdout] | [INFO] [stdout] 1512 | assert_sets_equal!(set1 == set2, elem => { [INFO] [stdout] | ^^^^^^^^^^^^^^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 1511 + use vstd::assert_sets_equal; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- tokens/frac.rs - tokens::frac::FracGhost (line 86) stdout ---- [INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found keyword `mut` [INFO] [stdout] --> tokens/frac.rs:88:17 [INFO] [stdout] | [INFO] [stdout] 88 | let tracked mut r = FracGhost::::new(123); [INFO] [stdout] | ^^^ expected one of `:`, `;`, `=`, `@`, or `|` [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- pervasive.rs - pervasive::struct_with_invariants (line 276) stdout ---- [INFO] [stdout] error: cannot find macro `struct_with_invariants` in this scope [INFO] [stdout] --> pervasive.rs:277:1 [INFO] [stdout] | [INFO] [stdout] 277 | struct_with_invariants!{ [INFO] [stdout] | ^^^^^^^^^^^^^^^^^^^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing one of these macros [INFO] [stdout] | [INFO] [stdout] 276 + use verus_builtin_macros::struct_with_invariants; [INFO] [stdout] | [INFO] [stdout] 276 + use vstd::prelude::struct_with_invariants; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- set_lib.rs - set_lib::assert_sets_equal (line 1505) stdout ---- [INFO] [stdout] error: cannot find macro `assert_sets_equal` in this scope [INFO] [stdout] --> set_lib.rs:1506:1 [INFO] [stdout] | [INFO] [stdout] 1506 | assert_sets_equal!(set1 == set2); [INFO] [stdout] | ^^^^^^^^^^^^^^^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 1505 + use vstd::assert_sets_equal; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: aborting due to 1 previous error [INFO] [stdout] [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- simple_pptr.rs - simple_pptr::PPtr (line 118) stdout ---- [INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope [INFO] [stdout] --> simple_pptr.rs:122:40 [INFO] [stdout] | [INFO] [stdout] 122 | let (p, Tracked(mut perm_p)) = PPtr::::empty(); [INFO] [stdout] | ^^^^ use of undeclared type `PPtr` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 119 + use vstd::simple_pptr::PPtr; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:122:17 [INFO] [stdout] | [INFO] [stdout] 122 | let (p, Tracked(mut perm_p)) = PPtr::::empty(); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope [INFO] [stdout] --> simple_pptr.rs:125:40 [INFO] [stdout] | [INFO] [stdout] 125 | let (q, Tracked(mut perm_q)) = PPtr::::empty(); [INFO] [stdout] | ^^^^ use of undeclared type `PPtr` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 119 + use vstd::simple_pptr::PPtr; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:125:17 [INFO] [stdout] | [INFO] [stdout] 125 | let (q, Tracked(mut perm_q)) = PPtr::::empty(); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:128:16 [INFO] [stdout] | [INFO] [stdout] 128 | p.free(Tracked(perm_p)); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:131:24 [INFO] [stdout] | [INFO] [stdout] 131 | let x = p.read(Tracked(&mut perm_q)); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error: aborting due to 6 previous errors [INFO] [stdout] [INFO] [stdout] Some errors have detailed explanations: E0425, E0433, E0531. [INFO] [stdout] For more information about an error, try `rustc --explain E0425`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- seq.rs - seq::seq (line 541) stdout ---- [INFO] [stdout] error: cannot find macro `seq` in this scope [INFO] [stdout] --> seq.rs:542:9 [INFO] [stdout] | [INFO] [stdout] 542 | let s = seq![11int, 12, 13]; [INFO] [stdout] | ^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 541 + use vstd::seq; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> seq.rs:544:1 [INFO] [stdout] | [INFO] [stdout] 544 | assert(s.len() == 3); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 544 | assert!(s.len() == 3); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> seq.rs:545:1 [INFO] [stdout] | [INFO] [stdout] 545 | assert(s[0] == 11); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 545 | assert!(s[0] == 11); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> seq.rs:546:1 [INFO] [stdout] | [INFO] [stdout] 546 | assert(s[1] == 12); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 546 | assert!(s[1] == 12); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> seq.rs:547:1 [INFO] [stdout] | [INFO] [stdout] 547 | assert(s[2] == 13); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 547 | assert!(s[2] == 13); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error: aborting due to 5 previous errors [INFO] [stdout] [INFO] [stdout] For more information about this error, try `rustc --explain E0423`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- tokens/map.rs - tokens::map (line 19) stdout ---- [INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found `sub2` [INFO] [stdout] --> tokens/map.rs:24:17 [INFO] [stdout] | [INFO] [stdout] 24 | let tracked sub2 = auth.insert_map(map![4u8 => 4u64, 5u8 => 5u64]); [INFO] [stdout] | ^^^^ expected one of `:`, `;`, `=`, `@`, or `|` [INFO] [stdout] [INFO] [stdout] error: cannot find macro `map` in this scope [INFO] [stdout] --> tokens/map.rs:21:57 [INFO] [stdout] | [INFO] [stdout] 21 | let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]); [INFO] [stdout] | ^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 19 + use vstd::map; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `GhostMapAuth` in this scope [INFO] [stdout] --> tokens/map.rs:21:39 [INFO] [stdout] | [INFO] [stdout] 21 | let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]); [INFO] [stdout] | ^^^^^^^^^^^^ use of undeclared type `GhostMapAuth` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 19 + use vstd::tokens::map::GhostMapAuth; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope [INFO] [stdout] --> tokens/map.rs:21:9 [INFO] [stdout] | [INFO] [stdout] 21 | let tracked (mut auth, mut sub) = GhostMapAuth::new(map![1u8 => 1u64, 2u8 => 2u64, 3u8 => 3u64]); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error: aborting due to 4 previous errors [INFO] [stdout] [INFO] [stdout] Some errors have detailed explanations: E0433, E0531. [INFO] [stdout] For more information about an error, try `rustc --explain E0433`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- tokens/frac.rs - tokens::frac::GhostVarAuth (line 335) stdout ---- [INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@` [INFO] [stdout] --> tokens/frac.rs:338:17 [INFO] [stdout] | [INFO] [stdout] 338 | assert(gauth@ == 1); [INFO] [stdout] | ^ expected one of 8 possible tokens [INFO] [stdout] [INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@` [INFO] [stdout] --> tokens/frac.rs:339:16 [INFO] [stdout] | [INFO] [stdout] 339 | assert(gvar@ == 1); [INFO] [stdout] | ^ expected one of 8 possible tokens [INFO] [stdout] [INFO] [stdout] error: expected one of `,`, `:`, or `}`, found `.` [INFO] [stdout] --> tokens/frac.rs:341:14 [INFO] [stdout] | [INFO] [stdout] 340 | proof { [INFO] [stdout] | ----- while parsing this struct [INFO] [stdout] 341 | gauth.update(&mut gvar, 2); [INFO] [stdout] | -----^ expected one of `,`, `:`, or `}` [INFO] [stdout] | | [INFO] [stdout] | while parsing this struct field [INFO] [stdout] | [INFO] [stdout] help: try naming a field [INFO] [stdout] | [INFO] [stdout] 341 | gauth: gauth.update(&mut gvar, 2); [INFO] [stdout] | ++++++ [INFO] [stdout] [INFO] [stdout] error: expected identifier, found `2` [INFO] [stdout] --> tokens/frac.rs:341:33 [INFO] [stdout] | [INFO] [stdout] 340 | proof { [INFO] [stdout] | ----- while parsing this struct [INFO] [stdout] 341 | gauth.update(&mut gvar, 2); [INFO] [stdout] | ^ expected identifier [INFO] [stdout] [INFO] [stdout] error: expected `;`, found `assert` [INFO] [stdout] --> tokens/frac.rs:342:6 [INFO] [stdout] | [INFO] [stdout] 342 | } [INFO] [stdout] | ^ help: add `;` here [INFO] [stdout] 343 | assert(gauth@ == 2); [INFO] [stdout] | ------ unexpected token [INFO] [stdout] [INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@` [INFO] [stdout] --> tokens/frac.rs:343:17 [INFO] [stdout] | [INFO] [stdout] 343 | assert(gauth@ == 2); [INFO] [stdout] | ^ expected one of 8 possible tokens [INFO] [stdout] [INFO] [stdout] error: expected one of `!`, `)`, `,`, `.`, `::`, `?`, `{`, or an operator, found `@` [INFO] [stdout] --> tokens/frac.rs:344:16 [INFO] [stdout] | [INFO] [stdout] 344 | assert(gvar@ == 2); [INFO] [stdout] | ^ expected one of 8 possible tokens [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `GhostVarAuth` in this scope [INFO] [stdout] --> tokens/frac.rs:337:41 [INFO] [stdout] | [INFO] [stdout] 337 | let tracked (mut gauth, mut gvar) = GhostVarAuth::::new(1); [INFO] [stdout] | ^^^^^^^^^^^^ use of undeclared type `GhostVarAuth` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 335 + use vstd::tokens::frac::GhostVarAuth; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope [INFO] [stdout] --> tokens/frac.rs:337:9 [INFO] [stdout] | [INFO] [stdout] 337 | let tracked (mut gauth, mut gvar) = GhostVarAuth::::new(1); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error: aborting due to 9 previous errors [INFO] [stdout] [INFO] [stdout] Some errors have detailed explanations: E0433, E0531. [INFO] [stdout] For more information about an error, try `rustc --explain E0433`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- simple_pptr.rs - simple_pptr::PPtr (line 92) stdout ---- [INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope [INFO] [stdout] --> simple_pptr.rs:97:43 [INFO] [stdout] | [INFO] [stdout] 97 | let (p, Tracked(mut points_to)) = PPtr::::empty(); [INFO] [stdout] | ^^^^ use of undeclared type `PPtr` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 93 + use vstd::simple_pptr::PPtr; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:97:17 [INFO] [stdout] | [INFO] [stdout] 97 | let (p, Tracked(mut points_to)) = PPtr::::empty(); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:100:17 [INFO] [stdout] | [INFO] [stdout] 100 | p.write(Tracked(&mut points_to), 5); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:103:24 [INFO] [stdout] | [INFO] [stdout] 103 | let x = p.read(Tracked(&points_to)); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:106:16 [INFO] [stdout] | [INFO] [stdout] 106 | p.free(Tracked(points_to)); // `points_to` is moved here [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:109:25 [INFO] [stdout] | [INFO] [stdout] 109 | let x2 = p.read(Tracked(&mut points_to)); // so it can't be used here [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error: aborting due to 6 previous errors [INFO] [stdout] [INFO] [stdout] Some errors have detailed explanations: E0425, E0433, E0531. [INFO] [stdout] For more information about an error, try `rustc --explain E0425`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- simple_pptr.rs - simple_pptr::PPtr (line 58) stdout ---- [INFO] [stdout] error: invalid comparison operator `===` [INFO] [stdout] --> simple_pptr.rs:65:41 [INFO] [stdout] | [INFO] [stdout] 65 | assert(points_to.mem_contents() === MemContents::Uninit); [INFO] [stdout] | ^^^ [INFO] [stdout] | [INFO] [stdout] help: `===` is not a valid comparison operator, use `==` [INFO] [stdout] | [INFO] [stdout] 65 - assert(points_to.mem_contents() === MemContents::Uninit); [INFO] [stdout] 65 + assert(points_to.mem_contents() == MemContents::Uninit); [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error: invalid comparison operator `===` [INFO] [stdout] --> simple_pptr.rs:71:41 [INFO] [stdout] | [INFO] [stdout] 71 | assert(points_to.mem_contents() === MemContents::Init(5)); [INFO] [stdout] | ^^^ [INFO] [stdout] | [INFO] [stdout] help: `===` is not a valid comparison operator, use `==` [INFO] [stdout] | [INFO] [stdout] 71 - assert(points_to.mem_contents() === MemContents::Init(5)); [INFO] [stdout] 71 + assert(points_to.mem_contents() == MemContents::Init(5)); [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `PPtr` in this scope [INFO] [stdout] --> simple_pptr.rs:63:43 [INFO] [stdout] | [INFO] [stdout] 63 | let (p, Tracked(mut points_to)) = PPtr::::empty(); [INFO] [stdout] | ^^^^ use of undeclared type `PPtr` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 59 + use vstd::simple_pptr::PPtr; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:63:17 [INFO] [stdout] | [INFO] [stdout] 63 | let (p, Tracked(mut points_to)) = PPtr::::empty(); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `MemContents` in this scope [INFO] [stdout] --> simple_pptr.rs:65:45 [INFO] [stdout] | [INFO] [stdout] 65 | assert(points_to.mem_contents() === MemContents::Uninit); [INFO] [stdout] | ^^^^^^^^^^^ use of undeclared type `MemContents` [INFO] [stdout] | [INFO] [stdout] help: consider importing this enum [INFO] [stdout] | [INFO] [stdout] 59 + use vstd::simple_pptr::MemContents; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `MemContents` in this scope [INFO] [stdout] --> simple_pptr.rs:71:45 [INFO] [stdout] | [INFO] [stdout] 71 | assert(points_to.mem_contents() === MemContents::Init(5)); [INFO] [stdout] | ^^^^^^^^^^^ use of undeclared type `MemContents` [INFO] [stdout] | [INFO] [stdout] help: consider importing this enum [INFO] [stdout] | [INFO] [stdout] 59 + use vstd::simple_pptr::MemContents; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> simple_pptr.rs:65:9 [INFO] [stdout] | [INFO] [stdout] 65 | assert(points_to.mem_contents() === MemContents::Uninit); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 65 | assert!(points_to.mem_contents() === MemContents::Uninit); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> simple_pptr.rs:66:9 [INFO] [stdout] | [INFO] [stdout] 66 | assert(points_to.pptr() == p); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 66 | assert!(points_to.pptr() == p); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:69:17 [INFO] [stdout] | [INFO] [stdout] 69 | p.write(Tracked(&mut points_to), 5); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> simple_pptr.rs:71:9 [INFO] [stdout] | [INFO] [stdout] 71 | assert(points_to.mem_contents() === MemContents::Init(5)); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 71 | assert!(points_to.mem_contents() === MemContents::Init(5)); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> simple_pptr.rs:72:9 [INFO] [stdout] | [INFO] [stdout] 72 | assert(points_to.pptr() == p); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 72 | assert!(points_to.pptr() == p); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:75:24 [INFO] [stdout] | [INFO] [stdout] 75 | let x = p.read(Tracked(&points_to)); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> simple_pptr.rs:77:9 [INFO] [stdout] | [INFO] [stdout] 77 | assert(x == 5); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 77 | assert!(x == 5); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error[E0425]: cannot find function, tuple struct or tuple variant `Tracked` in this scope [INFO] [stdout] --> simple_pptr.rs:80:30 [INFO] [stdout] | [INFO] [stdout] 80 | let y = p.into_inner(Tracked(points_to)); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error[E0423]: expected function, found macro `assert` [INFO] [stdout] --> simple_pptr.rs:82:9 [INFO] [stdout] | [INFO] [stdout] 82 | assert(y == 5); [INFO] [stdout] | ^^^^^^ not a function [INFO] [stdout] | [INFO] [stdout] help: use `!` to invoke the macro [INFO] [stdout] | [INFO] [stdout] 82 | assert!(y == 5); [INFO] [stdout] | + [INFO] [stdout] [INFO] [stdout] error: aborting due to 15 previous errors [INFO] [stdout] [INFO] [stdout] Some errors have detailed explanations: E0423, E0425, E0433, E0531. [INFO] [stdout] For more information about an error, try `rustc --explain E0423`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- tokens/seq.rs - tokens::seq::GhostSeqAuth (line 23) stdout ---- [INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found `sub2` [INFO] [stdout] --> tokens/seq.rs:28:17 [INFO] [stdout] | [INFO] [stdout] 28 | let tracked sub2 = sub.split(3); [INFO] [stdout] | ^^^^ expected one of `:`, `;`, `=`, `@`, or `|` [INFO] [stdout] [INFO] [stdout] error: cannot find macro `seq` in this scope [INFO] [stdout] --> tokens/seq.rs:25:57 [INFO] [stdout] | [INFO] [stdout] 25 | let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0); [INFO] [stdout] | ^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 23 + use vstd::seq; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `GhostSeqAuth` in this scope [INFO] [stdout] --> tokens/seq.rs:25:39 [INFO] [stdout] | [INFO] [stdout] 25 | let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0); [INFO] [stdout] | ^^^^^^^^^^^^ use of undeclared type `GhostSeqAuth` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 23 + use vstd::tokens::seq::GhostSeqAuth; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope [INFO] [stdout] --> tokens/seq.rs:25:9 [INFO] [stdout] | [INFO] [stdout] 25 | let tracked (mut auth, mut sub) = GhostSeqAuth::new(seq![0u64, 1u64, 2u64, 3u64, 4u64, 5u64], 0); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error: aborting due to 4 previous errors [INFO] [stdout] [INFO] [stdout] Some errors have detailed explanations: E0433, E0531. [INFO] [stdout] For more information about an error, try `rustc --explain E0433`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] ---- tokens/set.rs - tokens::set (line 20) stdout ---- [INFO] [stdout] error: expected one of `:`, `;`, `=`, `@`, or `|`, found `sub2` [INFO] [stdout] --> tokens/set.rs:25:17 [INFO] [stdout] | [INFO] [stdout] 25 | let tracked sub2 = auth.insert_set(set![4u8, 5u8]); [INFO] [stdout] | ^^^^ expected one of `:`, `;`, `=`, `@`, or `|` [INFO] [stdout] [INFO] [stdout] error: cannot find macro `set` in this scope [INFO] [stdout] --> tokens/set.rs:22:57 [INFO] [stdout] | [INFO] [stdout] 22 | let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]); [INFO] [stdout] | ^^^ [INFO] [stdout] | [INFO] [stdout] help: consider importing this macro [INFO] [stdout] | [INFO] [stdout] 20 + use vstd::set; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0433]: cannot find type `GhostSetAuth` in this scope [INFO] [stdout] --> tokens/set.rs:22:39 [INFO] [stdout] | [INFO] [stdout] 22 | let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]); [INFO] [stdout] | ^^^^^^^^^^^^ use of undeclared type `GhostSetAuth` [INFO] [stdout] | [INFO] [stdout] help: consider importing this struct [INFO] [stdout] | [INFO] [stdout] 20 + use vstd::tokens::set::GhostSetAuth; [INFO] [stdout] | [INFO] [stdout] [INFO] [stdout] error[E0531]: cannot find tuple struct or tuple variant `tracked` in this scope [INFO] [stdout] --> tokens/set.rs:22:9 [INFO] [stdout] | [INFO] [stdout] 22 | let tracked (mut auth, mut sub) = GhostSetAuth::new(set![1u8, 2u8, 3u8]); [INFO] [stdout] | ^^^^^^^ not found in this scope [INFO] [stdout] [INFO] [stdout] error: aborting due to 4 previous errors [INFO] [stdout] [INFO] [stdout] Some errors have detailed explanations: E0433, E0531. [INFO] [stdout] For more information about an error, try `rustc --explain E0433`. [INFO] [stdout] Couldn't compile the test. [INFO] [stdout] [INFO] [stdout] failures: [INFO] [stdout] arithmetic/overflow.rs - arithmetic::overflow (line 13) [INFO] [stdout] atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 230) [INFO] [stdout] atomic_ghost.rs - atomic_ghost::atomic_with_ghost (line 299) [INFO] [stdout] calc_macro.rs - calc_macro::calc (line 17) [INFO] [stdout] calc_macro.rs - calc_macro::calc (line 37) [INFO] [stdout] invariant.rs - invariant::open_atomic_invariant (line 355) [INFO] [stdout] invariant.rs - invariant::open_local_invariant (line 462) [INFO] [stdout] invariant.rs - invariant::open_local_invariant (line 483) [INFO] [stdout] invariant.rs - invariant::open_local_invariant (line 499) [INFO] [stdout] invariant.rs - invariant::open_local_invariant (line 508) [INFO] [stdout] map.rs - map::assert_maps_equal (line 355) [INFO] [stdout] map.rs - map::assert_maps_equal (line 368) [INFO] [stdout] pervasive.rs - pervasive::assert_by_contradiction (line 225) [INFO] [stdout] pervasive.rs - pervasive::struct_with_invariants (line 276) [INFO] [stdout] pervasive.rs - pervasive::struct_with_invariants (line 306) [INFO] [stdout] seq.rs - seq::seq (line 541) [INFO] [stdout] seq_lib.rs - seq_lib::assert_seqs_equal (line 3557) [INFO] [stdout] seq_lib.rs - seq_lib::assert_seqs_equal (line 3576) [INFO] [stdout] set_lib.rs - set_lib::assert_sets_equal (line 1505) [INFO] [stdout] set_lib.rs - set_lib::assert_sets_equal (line 1511) [INFO] [stdout] simple_pptr.rs - simple_pptr::PPtr (line 118) [INFO] [stdout] simple_pptr.rs - simple_pptr::PPtr (line 58) [INFO] [stdout] simple_pptr.rs - simple_pptr::PPtr (line 92) [INFO] [stdout] tokens/frac.rs - tokens::frac::FracGhost (line 86) [INFO] [stdout] tokens/frac.rs - tokens::frac::GhostVarAuth (line 335) [INFO] [stdout] tokens/map.rs - tokens::map (line 19) [INFO] [stdout] tokens/seq.rs - tokens::seq::GhostSeqAuth (line 23) [INFO] [stdout] tokens/set.rs - tokens::set (line 20) [INFO] [stdout] [INFO] [stdout] test result: FAILED. 1 passed; 28 failed; 7 ignored; 0 measured; 0 filtered out; finished in 1.51s [INFO] [stdout] [INFO] [stderr] error: doctest failed, to rerun pass `--doc` [INFO] running `Command { std: "docker" "inspect" "3ecafc2e3cf68d3c97bd89991b79e0678049b3c1f7dd8ce535d72ef360036e76", kill_on_drop: false }` [INFO] running `Command { std: "docker" "rm" "-f" "3ecafc2e3cf68d3c97bd89991b79e0678049b3c1f7dd8ce535d72ef360036e76", kill_on_drop: false }` [INFO] [stdout] 3ecafc2e3cf68d3c97bd89991b79e0678049b3c1f7dd8ce535d72ef360036e76