- Notifications
You must be signed in to change notification settings - Fork 13.9k
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.