Crate creusot_contracts

Source
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 of OrdLogic.
vec