CProver manual
|
Refers to the value of a given object in the pre-state of a function within the ensures clause.
Important. This function may be used only within the context of __CPROVER_ensures
.
__CPROVER_old
takes a single argument, which is the identifier corresponding to a parameter of the function. For now, only scalars, pointers, and struct members are supported.
To illustrate the behavior of __CPROVER_old
, take a look at the example bellow. If the function returns a failure code, the value of *out
should not have been modified.
TODO: Document __CPROVER_loop_entry
and __CPROVER_loop_old
.
Last modified: 2022-09-29 15:10:20 -0400