Backward-incompatible `prusti_contracts`

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.

http://prusti.org

Other

1.52k stars 103 forks source link

Backward-incompatible `prusti_contracts` #1446

Closed fpoli closed 5 months ago

fpoli commented 10 months ago

Because of the versioning issue reported last week, it's now no longer possible to verify, using an old Prusti release, crates that make use of prusti_contracts. Even specifying the following doesn't work; the error is always "[E0635] unknown feature extract_if."

[dependencies]
prusti-contracts = "=0.1.4"
prusti-contracts-proc-macros = "=0.1.4"

The error is[E0635] unknown feature 'extract_if', reported on .cargo/registry/src/github.../prusti-specs-0.1.10/src/lib.rs.

fpoli commented 10 months ago

This makes the test suite of prusti-assistant fail. For example: https://github.com/viperproject/prusti-assistant/pull/226