Contract variables can be declared in the `requires` clause and can be referenced both in `requires` and `ensures`, subject to usual borrow checking rules. This allows any setup common to both the `requires` and `ensures` clauses to only be done once.
18 lines
383 B
Rust
18 lines
383 B
Rust
//@ run-pass
|
|
#![feature(contracts)]
|
|
//~^ WARN the feature `contracts` is incomplete and may not be safe to use and/or cause compiler crashes [incomplete_features]
|
|
|
|
extern crate core;
|
|
use core::contracts::requires;
|
|
|
|
#[requires(*x = 0; true)]
|
|
fn buggy_add(x: &mut u32, y: u32) {
|
|
*x = *x + y;
|
|
}
|
|
|
|
fn main() {
|
|
let mut x = 10;
|
|
buggy_add(&mut x, 100);
|
|
assert_eq!(x, 110);
|
|
}
|