Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
Assertions about mutable references #
Assertions containing mutable references allow us to make statements about the prior (at the beginning of the function call) and current state of the piece of memory to which the mutable reference points. Consider the following example:
{{#include ../../../../examples/guide/references.rs:asserts}}
In the check_and_assert function call, *old(a) refers to the dereferenced value of the mutable reference a at the beginning of the function call and *a refers to the current dereferenced value of the mutable reference a.
Below is a slightly more complicated example involving both assert, requires, and ensures:
{{#include ../../../../examples/guide/references.rs:complex}}