Enum Assumption 

pub enum Assumption {
    Approaching,
    NoWrap(Chrec),
    StrictOverflow,
}

Something that has to be true for a trip count to be the right answer.

Section 7.5 asks for exactly this: not a trip count but a trip count plus a predicate under which it holds, so the consumer either proves the predicate, emits a runtime check for it, or gives up. These are the predicates.

Variants

Approaching

The counter starts on the near side of its limit, so the distance between them is a number that is not negative.

For a loop ending on an ordering this is the loop being entered at all. for (i = 0; i < n; i++) with n of zero runs no times and the distance is zero, but n of minus one also runs no times and the distance is minus one, so a count taken from the distance has to be told which case it is in. For a loop ending on != it is the limit being somewhere the counter is heading, because one stepping away from its limit never arrives.

Only ever present on a symbolic count. When the distance is a number the sign of it is there to be read, so this is settled rather than assumed.

NoWrap(Chrec)

The induction variable does not wrap in its own type before the exit is taken.

Present whenever the increment did not carry the matching nsw or nuw flag. With the flag there is nothing to assume, because the flag is the promise.

StrictOverflow

Signed overflow is undefined here, which is what makes for (int i = 0; i <= n; i++) finite.

GCC infers loop bounds from this in infer_loop_bounds_from_signedness, and it is the single most common source of a report that the compiler broke a working program. It is recorded rather than assumed silently so that -fwrapv can withdraw the count and so that a dump can name it.

Implementations

impl Assumption

pub fn describe(&self) -> String

What it says, in a line, for a dump to print.

Section 7.5 asks that every inference of this kind be dumpable and say what it rests on, because a user who has been bitten by one deserves a command that tells them which line the compiler used against them. This is the sentence that command prints.

Trait Implementations

impl Clone for Assumption

fn clone(&self) -> Assumption

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for Assumption

impl Debug for Assumption

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Eq for Assumption

impl PartialEq for Assumption

fn eq(&self, other: &Assumption) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Assumption