When verifying a C function, we need to specify its contract at the beginning of the function using annotations. This contract describes the function's safety or functional correctness. A C function's specification consists of a logical parameter list (With) and the corresponding separation logic pre- and postconditions (Require, Ensure). In simple cases, the specification may omit the With list.
Example 1: Adding Two Numbers
The following C function adds two signed integer arguments and returns the result (found in simple_arith/add.c).
int add(int x, int y)
/*@ Require
0 <= x && x <= 100 &&
0 <= y && y <= 100
Ensure
__return == x + y
*/
{
int z;
z = x + y;
return z;
}
In this code, the Require condition states that both arguments of the add function are between 0 and 100; the Ensure condition states that the return value equals the sum of the two arguments. Together, these two conditions form the specification of this C function: if both arguments are between 0 and 100, then the function is guaranteed to execute safely and return their sum. Here, "guaranteed to execute safely" means that no undefined behavior (UB) as defined by the C standard will occur. Typical examples of UB include division by zero, signed integer overflow, out-of-bounds array access, and null pointer dereference. Since the C standard specifies that signed integer overflow is UB, restricting the range of the two arguments in the example above is necessary. In other words, the above C function does not satisfy the following specification:
int add(int x, int y)
/*@ Require
True
Ensure
__return == x + y
*/
Of course, the constraint range can be relaxed as follows.
int add_tight(int x, int y)
/*@ Require
INT_MIN <= x + y && x + y <= INT_MAX
Ensure
__return == x + y
*/
{
int z;
z = x + y;
return z;
}
It is also worth noting that x and y in the Ensure assertion refer to their values at the time they were passed into the function. Therefore, the following C function satisfies the same specification.
int add_alter1(int x, int y)
/*@ Require
0 <= x && x <= 100 &&
0 <= y && y <= 100
Ensure
__return == x + y
*/
{
x = x + y;
return x;
}
Naturally, a C function that directly computes and returns the result without variable assignment also satisfies the same specification.
int add_alter2(int x, int y)
/*@ Require
0 <= x && x <= 100 &&
0 <= y && y <= 100
Ensure
__return == x + y
*/
{
return x + y;
}
Example 2: Modifying Memory Contents
In the following example, the C function takes an address as its argument and modifies the value stored at that address (found in simple_arith/add.c).
void add1_ptr(int * x)
{
* x ++;
}
To describe the relationship between the value of * x when the function returns and its original value, we need a With variable.
void add1_ptr(int * x)
/*@ With (v: Z)
Require (INT_MIN <= v) && (v < INT_MAX) &&
* x == v
Ensure * x == v + 1 */
This specification states: for any integer v satisfying INT_MIN <= v && v < INT_MAX, if the value stored at address x is v before executing the function, then the function is guaranteed to execute safely, and upon return the value stored at address x will become v + 1. In other words, With here expresses universal quantification ("for all"). Note that the formal parameter x in the Ensure condition refers to the value of x at the time it was passed into the function, while * x does not refer to the initial value at address x, but rather the value at that address when the function call completes. Specifically, a formal parameter itself represents its value when passed into the function, whereas other operations -- particularly the dereference operator (asterisk) -- represent the result of reading memory at the time the function returns.