QCP Tutorials Memory and Assertions

If a and b are two signed integer global variables in a C program, then the following three versions of the swap_ab function can all swap their values.

int a;
int b;

void swap_ab()
{
  int t;
  t = a;
  a = b;
  b = t;
}

void swap_ab_alter1()
{
  swap(&a, &b);
}

void swap_ab_alter2()
{
  swap(&b, &a);
}

To describe the behavior of such programs, you can use the addresses of global variables together with the separation logic predicate store to construct the Require and Ensure conditions.

void swap_ab()
/*@ With x y
    Require store_int(&a, x) * store_int(&b, y)
    Ensure store_int(&a, y) * store_int(&b, x) */
;