Expand description
The “standard library” of Creusot.
To start using Creusot, you should always import that crate. The recommended way is to have a glob import:
use creusot_contracts::*;
§Writing specifications
To start writing specification, use the requires
and ensures
macros:
use creusot_contracts::*;
#[requires(x < i32::MAX)]
#[ensures(result@ == x@ + 1)]
fn add_one(x: i32) -> i32 {
x + 1
}
For a more detailed explanation, see the guide.
Re-exports§
pub use prelude::*;
Modules§
- ghost
- Definitions for ghost code
- invariant
- logic
- Definitions for pearlite code
- macros
- Specification are written using these macros
- model
- num_
rational - pcell
- Shared mutation with a ghost token
- prelude
- ptr_own
- Raw pointers with ghost code
- resolve
- snapshot
- Definition of
Snapshot
- std
- util
- Some useful logical items
- well_
founded
Macros§
- ord_
laws_ impl - A macro to easily implements the various
#[law]
s ofOrdLogic
. - vec