prusti-contracts
| Crates.io | prusti-contracts |
| lib.rs | prusti-contracts |
| version | 0.2.0 |
| source | src |
| created_at | 2022-09-26 13:37:48.523549 |
| updated_at | 2023-09-04 12:27:01.668662 |
| description | Tools for specifying contracts with Prusti |
| homepage | https://www.pm.inf.ethz.ch/research/prusti.html |
| repository | https://github.com/viperproject/prusti-dev/tree/master/prusti-contracts/prusti-contracts/ |
| max_upload_size | |
| id | 674256 |
| size | 14,979 |
(prusti-devs)
documentation
README
Provides various macros and types needed for verification of a crate with Prusti. See the Prusti user guide or GitHub page for more information.
When used without Prusti (e.g. with cargo build) this crate will be as transparent as possible and does not need to be removed from the dependencies. When running cargo prusti the "prusti" feature is automatically enabled, resulting in the full expansion of the procedural macros this crate provides.