Module macros 

Specification are written using these macros

All of those are re-exported at the top of the crate.

Macros

extern_spec

Allows specifications to be attached to functions coming from external crates

ghost

Opens a ‘ghost block’.

ghost_let

pearlite

Enables pearlite syntax, granting access to Pearlite specific operators and syntax

proof_assert

Inserts a logical assertion into the code

snapshot

Create a new Snapshot object.

Attribute Macros

bitwise_proof

This attribute indicates that the function need to be proved in “bitwise” mode, which means that Creusot will use the bitvector theory of SMT solvers.

builtin

This attribute indicates that a logic function or a type should be translated to a specific type in Why3.

check

Specify that the function can be called in additionnal contexts.

ensures

A post-condition of a function or trait item

erasure

Check that the annotated function erases to another function.

invariant

A loop invariant

logic

Declare a function as being a logical function

maintains

Allows specifying both a pre- and post-condition in a single statement.

opaque

Makes a logical definition or a type declaration opaque, meaning that users of this declaration will not see its definition.

open_inv_result

This attribute can be used on a function or closure to instruct Creusot not to ensure as a postcondition that the return value of the function satisfies its type invariant.

requires

A pre-condition of a function or trait item

trusted

Instructs Creusot to not emit any VC for a declaration, assuming any contract the declaration has is valid.

variant

Declares a variant for a function or a loop.