CBMC
History Variables

Table of Contents

Back to Code Contracts User Documentation

In Function Contracts

Syntax

__CPROVER_old(*identifier*)
__CPROVER_old
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 */
__CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out)))
/* Writable Set */
__CPROVER_assigns(*out)
{
/* ... */
}

In Loop Contracts

Syntax

__CPROVER_loop_entry(*identifier*)
__CPROVER_loop_entry
void __CPROVER_loop_entry(const void *)

Parameters

__CPROVER_loop_entry takes a variable name that is in scope at the place of the loop contract.

Semantics

__CPROVER_loop_entry takes a snapshot of the variable value right before the first iteration of the loop. Caveat: to create a snapshot of an array, cast the array variable (which is a pointer per C's type system) to a pointer-to-array, and then dereference.

typedef int array_type[2];
array_type var;
__CPROVER_loop_invariant(__CPROVER_loop_entry(*(array_type*)var)[0] <= 42)

Example

In this example the loop invariant asserts that x <= 200 is upheld before and after every iteration of the while loop:

void my_function()
{
unsigned x = 200;
while( x >= 64 )
__CPROVER_loop_invariant(x <= __CPROVER_loop_entry(x)) //equivalent to x <= 200
{
...
x -= 64;
}
}

Additional Resources