P0007

Postcondition violated: an ensures clause of the function that returned is false, so the function broke its promise. The message names the function, quotes the clause's condition, and names the line and column of the return that broke it, counting columns in characters from 1. Spans the ensures clause. Every return evaluates the function's ensures clauses, in every build, in the order written, with r bound to the value being returned. That covers falling off the end of the body (the return is its last expression, or its closing brace), an early return, and an early exit through ?, where r is the Err or None being returned. A clause sees the parameters and self; a method that changes var self shows its clauses the receiver it ends with. A contract that calls a function with contracts checks those too, and a panic while a clause is evaluated, such as an overflow, is reported as it is, not as P0007.

Machine-applicable fix: none.

Example

This program fails with P0007.

fn absolute(x: Int) -> Int
    ensures |r| r >= 0
{
    x
}

fn main() {
    let y = absolute(-1)
}

Fixed

The same program, fixed.

fn absolute(x: Int) -> Int
    ensures |r| r >= 0
{
    if x < 0 {
        0 - x
    } else {
        x
    }
}

fn main() {
    let y = absolute(-1)
}

Listed in the runtime notes. oskac explain P0007 prints this entry offline.

All error codes