cprover
Loading...
Searching...
No Matches
History Variables

Back to Code Contracts User Documentation

In Function Contracts

Syntax

__CPROVER_old(*identifier*)
void __CPROVER_old(const void *)

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.

Parameters

__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.

Semantics

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.

int sum(const uint32_t a, const uint32_t b, uint32_t* out)
/* Postconditions */
/* Writable Set */
{
/* ... */
}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563

In Loop Contracts

TODO: Document __CPROVER_loop_entry and __CPROVER_loop_old.

Additional Resources