demonstrate how to capture state at precondition time and feed into postcondition predicate.

Author: pnkfelix

tests/ui/contracts/contract-captures-via-closure-copy.rs

@@ -0,0 +1,25 @@
+//@ run-fail
+//@ compile-flags: -Zcontract-checks=yes
+
+#![feature(rustc_contracts)]
+
+struct Baz {
+    baz: i32
+}
+
+#[track_caller]
+#[core::contracts::requires(x.baz > 0)]
+#[core::contracts::ensures({let old = x.baz; move |ret:&Baz| ret.baz == old*2 })]
+// Relevant thing is this:  ^^^^^^^^^^^^^^^
+// because we are capturing state that is Copy
+fn doubler(x: Baz) -> Baz {
+    Baz { baz: x.baz + 10 }
+}
+
+fn main() {
+    assert_eq!(doubler(Baz { baz: 10 }).baz, 20);
+    assert_eq!(doubler(Baz { baz: 100 }).baz, 200);
+    // This is a *run-fail* test because it is still exercising the
+    // contract machinery, specifically because this second invocation
+    // of `doubler` shows how the code does not meet its contract.
+}

tests/ui/contracts/contract-captures-via-closure-noncopy.rs

@@ -0,0 +1,22 @@
+//@ compile-flags: -Zcontract-checks=yes
+
+#![feature(rustc_contracts)]
+
+struct Baz {
+    baz: i32
+}
+
+#[track_caller]
+#[core::contracts::requires(x.baz > 0)]
+#[core::contracts::ensures({let old = x; move |ret:&Baz| ret.baz == old.baz*2 })]
+// Relevant thing is this:  ^^^^^^^^^^^
+// because we are capturing state that is non-Copy.
+//~^^^ ERROR trait bound `Baz: std::marker::Copy` is not satisfied
+fn doubler(x: Baz) -> Baz {
+    Baz { baz: x.baz + 10 }
+}
+
+fn main() {
+    assert_eq!(doubler(Baz { baz: 10 }).baz, 20);
+    assert_eq!(doubler(Baz { baz: 100 }).baz, 200);
+}

tests/ui/contracts/contract-captures-via-closure-noncopy.stderr

@@ -0,0 +1,27 @@
+error[E0277]: the trait bound `Baz: std::marker::Copy` is not satisfied in `{closure@$DIR/contract-captures-via-closure-noncopy.rs:11:42: 11:57}`
+  --> $DIR/contract-captures-via-closure-noncopy.rs:11:1
+   |
+LL | #[core::contracts::ensures({let old = x; move |ret:&Baz| ret.baz == old.baz*2 })]
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^------------------------------------^^^^
+   | |                                        |
+   | |                                        within this `{closure@$DIR/contract-captures-via-closure-noncopy.rs:11:42: 11:57}`
+   | |                                        this tail expression is of type `{[email protected]:11:42}`
+   | unsatisfied trait bound
+   |
+   = help: within `{closure@$DIR/contract-captures-via-closure-noncopy.rs:11:42: 11:57}`, the trait `std::marker::Copy` is not implemented for `Baz`
+note: required because it's used within this closure
+  --> $DIR/contract-captures-via-closure-noncopy.rs:11:42
+   |
+LL | #[core::contracts::ensures({let old = x; move |ret:&Baz| ret.baz == old.baz*2 })]
+   |                                          ^^^^^^^^^^^^^^^
+note: required by a bound in `build_check_ensures`
+  --> $SRC_DIR/core/src/contracts.rs:LL:COL
+help: consider annotating `Baz` with `#[derive(Copy)]`
+   |
+LL + #[derive(Copy)]
+LL | struct Baz {
+   |
+
+error: aborting due to 1 previous error
+
+For more information about this error, try `rustc --explain E0277`.