Attribute Macro check 

#[check]

Specify that the function can be called in additionnal contexts.

Syntax

Checking modes are specified as arguments:

#[check(terminates)]
fn foo() { /* */ }

#[check(ghost)]
fn bar() { /* */ }

// cannot be called in neither ghost nor terminates contexts
fn baz() { /* */ }

#[check(terminates)]

The function is guaranteed to terminate.

At this moment, this means that:

• the function cannot be recursive
• the function cannot contain loops
• the function can only call other terminates or ghost functions.

The first two limitations may be lifted at some point.

#[check(ghost)]

The function can be called from ghost code. In particular, this means that the fuction will not panic.

No panics ?

“But I though Creusot was supposed to check the absence of panics ?”

That’s true, but with a caveat: some functions of the standard library are allowed to panic in specific cases. The main example is Vec::push: we want its specification to be

#[ensures((^self)@ == self@.push(v))]
fn push(&mut self, v: T) { /* ... */ }

But the length of a vector cannot overflow isize::MAX. This is a very annoying condition to check, so we don’t. In exchange, this means Vec::push might panic in some cases, even though your code passed Creusot’s verification.

Non-ghost std function

Here are some examples of functions in std that are not marked as terminates but not ghost (this list is not exhaustive):

• Vec::push, Vec::insert, Vec::reserve, Vec::with_capacity
• str::to_string
• <&[T]>::into_vec
• Deque::push_front, Deque::push_back, Deque::with_capacity