QCP Tutorials Memory and Assertions

If a C program defines the following struct struct int_pair, it is natural to use the previously defined swap function to swap the values of its two fields.

struct int_pair {
    int a;
    int b;
};

void swap_int_pair(struct int_pair * p)
{
  swap(&(p -> a), &(p -> b));
}

We can use the same approach as before to describe the specification of the swap_int_pair function:

void swap_int_pair(struct int_pair * p)
/*@ With x y
    Require store_int(&(p -> a), x) * store_int(&(p -> b), y)
    Ensure store_int(&(p -> a), y) * store_int(&(p -> b), x) */
{
  swap(&(p -> a), &(p -> b));
}

As you can see, QCP allows C expressions such as &(p -> a) to be used in assertions to denote an address. Apart from this, the assertions in this specification are essentially the same as those for the swap function.

QCP does not currently support verification of C functions that take structs directly as parameters, but it does allow struct pointers as function parameters, as shown in the example above.