Attribute Macro pre::pre

#[pre]

Specify preconditions on functions and check that they are assured correctly for calls.

Its counterpart is the assure attribute.

Basic usage example

Suppose you have a precondition stating that a function use_foo must only be called after some other initialization function init_foo was called. You could add that precondition to the use_foo function as follows:

use pre::pre;

#[pre("is only called after `init_foo` was called")]
fn use_foo(/* ... */) {
    /* ... */
}

To call the function use_foo now, you have to assure that the precondition holds.

Note that the precondition states how things are if everything goes well and not how they should be. This makes it easier to read code calling the function.

Precondition syntax

There are multiple different types of preconditions that you can use for your functions:

1. Custom preconditions:

   This is the simplest kind of precondition. It is a string describing the condition.

   The syntax is #[pre("<string>")].

   • <string>: An arbitrary string describing the condition.

   Example

   #[pre("describe your precondition here")]
   fn foo() {}

2. Valid pointer preconditions:

   This precondition requires that a raw pointer is valid for reads or writes or both.

   The syntax is #[pre(valid_ptr(<ptr_name>, <access_modes>))].

   • <ptr_name>: The identifier of the pointer argument that must be valid.
   • <access_modes>: One of r, w or r+w. This specifies whether the pointer is valid for reads (r) or writes (w) or both (r+w).

   Example

   #[pre(valid_ptr(ptr_name, r+w))]
   fn foo(ptr_name: *mut i32) {}

   This precondition does not guarantee:

   • A proper alignment of the pointer.
   • A valid initialized value for the pointee.

   Also there are no guarantees about the size of the allocated object. If there are no other preconditions about the size of the allocated object, usually the size of a single value can be assumed.

3. Proper alignment preconditions:

   This precondition requires that a raw pointer has a proper alignment for its type. More concretely for a *const T and *mut T, this means that the pointer must have an alignment of mem::align_of::<T>().

   The syntax is #[pre(proper_align(<ptr_name>))].

   • <ptr_name>: The identifier of the pointer argument that must have a proper alignment.

   Example

   #[pre(proper_align(ptr_name))]
   fn foo(ptr_name: *mut i32) {}

4. Boolean preconditions:

   This precondition is a boolean expression that should evaluate to true for the precondition to hold. By default a debug_assert statement is added to the function for such a precondition. This can be disabled by a #[pre(no_debug_assert)] attribute.

   The syntax is #[pre(<expr>)].

   • <expr>: A boolean expression that should evaluate to true.

   Example

   #[pre(a < b || b > 17)]
   fn foo(a: i32, b: i32) {}

General syntax

There are three uses of the pre attribute:

1. Specify one or multiple preconditions (for the exact syntax of the preconditions, see "Precondition syntax"):

   #[pre(<first precondition>)]
   #[pre(<second precondition>)]
   #[pre(<third precondition>)]
   fn foo() {}

2. Enable handling of assure and forward attributes for the annotated item (see "Checking functionality"):

   #[pre]
   fn main() {
       // `assure` and `forward` attributes here are properly handled.
   }

   This works with any of the forms of the pre attribute, but in case no other functionality is needed, a bare #[pre] can be used.

3. Disable generating documentation for the preconditions (see "Documentation on items with preconditions"):

   #[pre(no_doc)]
   #[pre("some precondition")]
   fn foo() {} // foo will not have any documentation generated by pre.

4. Disable debug assertions for boolean preconditions.

   #[pre(no_debug_assert)]
   #[pre(old_val < new_val)]
   fn foo() {} // foo will not have any `debug_assert`s generated by pre.

Checking functionality

The pre attribute can also be used to enable the functionalities of the assure and forward attributes for the item it is attached to. In this case it can be left empty: #[pre]. Any other form of a pre attribute being present on an item renders the empty one obsolete though, as any of its forms enables this functionality.

Doing this is currently necessary, because the current (1.44.1) stable rust compiler does not support attribute macros being applied to statements or expressions directly.

Documentation on items with preconditions

Items annotated with one or more preconditions have information about their preconditions and how to call them with the preconditions appended at the end of their documentation.

If you wish not to add such documentation to a particular item, you can add #[pre(no_doc)] to the attributes of the item to prevent its generation.