Attribute Macro creusot_contracts::macros::pure

#[pure]

Indicate that the function is pure: fulfilling the requires clauses ensures that this function will terminate, and 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 require, so we don’t. In exchange, this means Vec::push might panic in some cases, even though your code passed Creusot’s verification.

Non-pure std function

Here are some examples of functions in std that are not marked as terminates but not pure (this list might not be 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