Vx

E8001

Error · Contract/Verification

E8001 — Cannot prove postcondition

What the compiler reports

Error[E8001] … Function 'incorrect_postcondition' cannot prove postcondition

The fragments the test suite holds the compiler to. An ellipsis marks text the test does not constrain; the emitted message also carries a source location.

A program that triggers it

import core::convert;

fn incorrect_postcondition(value : i32) -> i64
ensures return != value {
  return i64::from(value);
}

fn main() -> i32 {
  return incorrect_postcondition(17) as i32;
}

From tests/frontend/fail/formal_verification/i32_to_i64_cannot_claim_a_different_value.vx, which asserts this diagnostic on every commit.

Related

Contracts and verificationThe chapter covering the rule this code enforces. All diagnosticsEvery code the compiler can emit, grouped by stage. E8002Comptime assert failed