This captures one of the issues raised by @zhassan-aws (#1213 (comment))
Try the following steps:
cargo new --lib lstd
- Put the following in
src/lib.rs:
#[kani::proof]
fn check_format() {
assert!("2021".parse::<u32>().unwrap() == 2021);
}
- Build using:
KANIFLAGS="--goto-c --ignore-global-asm --log-level=error --assertion-reach-checks -C symbol-mangling-version=v0" RUSTC="/home/ubuntu/git/kani/target/debug/kani-compiler" RUSTFLAGS="--kani-flags" cargo +nightly-2022-05-17 build --target x86_64-unknown-linux-gnu -Z build-std --lib --target-dir target
The following errors are emitted:
error: duplicate lang item in crate `std` (which `kani` depends on): `panic_impl`.
|
= note: the lang item is first defined in crate `std` (which `lstd` depends on)
= note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
= note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib
error: duplicate lang item in crate `std` (which `kani` depends on): `begin_panic`.
|
= note: the lang item is first defined in crate `std` (which `lstd` depends on)
= note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
= note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib
error: duplicate lang item in crate `std` (which `kani` depends on): `oom`.
|
= note: the lang item is first defined in crate `std` (which `lstd` depends on)
= note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
= note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib
error: duplicate lang item in crate `std` (which `kani` depends on): `start`.
|
= note: the lang item is first defined in crate `std` (which `lstd` depends on)
= note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
= note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib
error: duplicate lang item in crate `std` (which `kani` depends on): `termination`.
|
= note: the lang item is first defined in crate `std` (which `lstd` depends on)
= note: first definition in `std` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libstd-9f9e8af9b2102e2a.rmeta
= note: second definition in `std` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libstd-977ece543e1e3d2f.rlib
error: duplicate lang item in crate `core` (which `std` depends on): `sized`.
|
= note: the lang item is first defined in crate `core` (which `std` depends on)
= note: first definition in `core` loaded from /home/ubuntu/examples/lstd/target/x86_64-unknown-linux-gnu/debug/deps/libcore-6d9d14315cbfc8dc.rmeta
= note: second definition in `core` loaded from /home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/x86_64-unknown-linux-gnu/lib/libcore-0e3656b1fda5fd7b.rlib
error[E0034]: multiple applicable items in scope
--> src/lib.rs:3:20
|
3 | assert!("2021".parse::<u32>().unwrap() == 2021);
| ^^^^^ multiple `parse` found
|
= note: candidate #1 is defined in an impl for the type `str`
= note: candidate #2 is defined in an impl for the type `str`
For more information about this error, try `rustc --explain E0034`.
Error: "Failed to compile crate."
error: could not compile `lstd` due to 113 previous errors
Edited from @zhassan-aws original post in #1213 (comment)
This captures one of the issues raised by @zhassan-aws (#1213 (comment))
Try the following steps:
cargo new --lib lstdsrc/lib.rs:The following errors are emitted:
Edited from @zhassan-aws original post in #1213 (comment)