prusti-dev
prusti-dev copied to clipboard
`cargo prusti -vv` fails verification in crate dependencies
Running cargo prusti -vv (very verbose output) will lead to many [Prusti: unsupported feature] errors in dependencies of the current crate, and failing verification of the crate.
One example is a crate with just an empty main function, and a dependency on syn in Cargo.toml:
[dependencies]
syn = "2.0.14"
This is the output (removed rustc commands in [...]):
$ cargo prusti -vv
Compiling proc-macro2 v1.0.56
Checking unicode-ident v1.0.8
Compiling quote v1.0.26
Running [...]
Running `CARGO=/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/bin/cargo
CARGO_CRATE_NAME=unicode_ident
CARGO_MANIFEST_DIR=/.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8
CARGO_PKG_AUTHORS='David Tolnay <[email protected]>'
CARGO_PKG_DESCRIPTION='Determine whether characters have the XID_Start or XID_Continue properties according to Unicode Standard Annex #31'
CARGO_PKG_HOMEPAGE='' CARGO_PKG_LICENSE='(MIT OR Apache-2.0) AND Unicode-DFS-2016'
CARGO_PKG_LICENSE_FILE='' CARGO_PKG_NAME=unicode-ident
CARGO_PKG_REPOSITORY='https://github.com/dtolnay/unicode-ident'
CARGO_PKG_RUST_VERSION=1.31 CARGO_PKG_VERSION=1.0.8 CARGO_PKG_VERSION_MAJOR=1
CARGO_PKG_VERSION_MINOR=0 CARGO_PKG_VERSION_PATCH=8 CARGO_PKG_VERSION_PRE=''
LD_LIBRARY_PATH='prusti-vv-bug/target/verify/debug/deps:.rustup/toolchains/nightly-2023-03-08-x86_64-unknown-linux-gnu/lib:/.rustup/toolchains/nightly-2023-03-08-x86_64-unknown-linux-gnu/lib:/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib'
prusti-rustc --crate-name unicode_ident
--edition=2018 /.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8/src/lib.rs
--error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat
--diagnostic-width=237 --crate-type lib --emit=dep-info,metadata
-C embed-bitcode=no -C debuginfo=2 -C metadata=4568e78affd58b00
-C extra-filename=-4568e78affd58b00 --out-dir prusti-vv-bug/target/verify/debug/deps
-L dependency=prusti-vv-bug/target/verify/debug/deps
--cap-lints warn`
Running [...]
error: [Prusti: unsupported feature] unsupported constant type Ref('_#6r, tables::Align64<[bool; 128]>, Not)
--> /.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8/src/lib.rs:255:16
|
255 | return ASCII_START.0[ch as usize];
| ^^^^^^^^^^^
error: [Prusti: unsupported feature] unsupported constant type Ref('_#6r, tables::Align64<[bool; 128]>, Not)
--> /.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8/src/lib.rs:264:16
|
264 | return ASCII_CONTINUE.0[ch as usize];
| ^^^^^^^^^^^^^^
error: could not compile `unicode-ident` due to 2 previous errors
Caused by:
process didn't exit successfully: [...]
(exit status: 1)
warning: build failed, waiting for other jobs to finish...
Running cargo prusti without the -vv flag will verify this test crate correctly.
Other dependencies such as prusti-contracts also cause errors with the -vv flag.
The flag be_rustc should be set when compiling the dependencies, which should prevent these errors.