Contracts allow side effect expressions
@celinval is already working on this.
Since Apr 8, 2025.
- Dominant language
- Rust
- Stars
- 119k
- Forks
- 16.1k
- PR merge metrics
- PR metrics pending
Description
I tried this code:
#![feature(contracts)]
#[core::contracts::ensures({*x = 0; |_ret| 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);
}
I expected to see this happen: The assertions should succeed
Instead, this happened: The assertion fails because x == 100. Note that this bad behavior happens even with the contract checks disabled. I.e.: with -Zcontract-checks=no
Meta
rustc --version --verbose:
rustc 1.86.0 (05f9846f8 2025-03-31)
binary: rustc
commit-hash: 05f9846f893b09a1be1fc8560e33fc3c815cfecb
commit-date: 2025-03-31
host: x86_64-unknown-linux-gnu
release: 1.86.0
LLVM version: 19.1.7
Context
We currently instantiate the ensures clause in the function body as is. This logic is different than how we handle requires, where we wrap it around a closure. This has a neat property that allow users to capture input values to implement old terms.
Unfortunately, this allows users to also mutate the input, which is rather dangerous. So I believe we should also wrap the ensures clause in a closure. We can keep the capture input behavior, but this will create another layer of indirection.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Assessment
This issue has not been assessed yet.