Crate creusot_contracts

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
• 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