21 lines
534 B
Rust
21 lines
534 B
Rust
// error-pattern:Unsatisfied precondition constraint (for example, le(b, d
|
|
use std;
|
|
import std::str::*;
|
|
import std::uint::*;
|
|
|
|
fn main() {
|
|
let a: uint = 1u;
|
|
let b: uint = 4u;
|
|
let c: uint = 5u;
|
|
// make sure that the constraint le(b, a) exists...
|
|
check (le(b, a));
|
|
// ...invalidate it...
|
|
b += 1u;
|
|
check (le(c, a));
|
|
// ...and check that it doesn't get set in the poststate of
|
|
// the next statement, since it's not true in the
|
|
// prestate.
|
|
let d <- a;
|
|
log safe_slice("kitties", b, d);
|
|
}
|