关于Ensure断言的验证条件
swap函数的例子
下面是之前提到过的swap函数。
void swap(int * px, int * py)
/*@ With x y
Require store_int(px, x) * store_int(py, y)
Ensure store_int(px, y) * store_int(py, x) */
{
int t;
t = * px;
* px = * py;
* py = t;
}
在该C函数的验证过程中，QCP符号执行系统会依次处理“进入函数体”、“变量声明”、“赋值语句”和“退出函数体”，最后生成如下断言：
store_int(px_37, y) *
store_int(py_40, x)
其中px_37与py_40分别对应px_58和py@pre。而Ensure条件实际也是
store_int(px_37, y) *
store_int(py_40, x)
此时，QCP符号执行器就会生成下面验证条件。这表示，只要该验证条件成立，那么swap函数就满足Require和Ensure断言所描述的规约。
store_int(px_37, y) *
store_int(py_40, x)
|--
store_int(px_37, y) *
store_int(py_40, x)
swap函数的弱化版本
如果修改上面swap函数的Ensure条件，
void swap(int * px, int * py)
/*@ With x y
Require store_int(px, x) * store_int(py, y)
Ensure has_int_permission(px) *
has_int_permission(py) */
{
int t;
t = * px;
* px = * py;
* py = t;
}
那么这就描述了一个较弱的安全性性质，即swap之后依旧拥有px和py这两个地址的读写权限，但是其中存储内容是否初始化过都不做保障。
由于Require条件没有改变，符号执行依然会得到与先前同样的断言。因此，QCP的符号执行器就会生成以下验证条件。
store_int(px_37, y) *
store_int(py_40, x)
|--
has_int_permission(px_37) *
has_int_permission(py_40)
显然，这个验证条件成立，因此，QCP工具就可以确认swap满足弱化之后的规约。
表达式计算的附加条件
C语言不保证任何一个表达式的能在任何情况下安全完成求值。例如，空指针解引用、悬空指针解引用、数组下标越界、除数为零等。QCP验证工具验证C程序时就会检验以确保不出现这些情况。
QCP工具采取的验证方法是在符号执行的过程中检验相应的安全性条件。上面这些程序出错类型中，有一些会直接阻碍符号执行的立即执行。例如，对于赋值语句t = * px而言，如果QCP在断言中找不到相应的store谓词，那么就无法用断言将该语句执行后程序状态所满足的条件表述出来。如果C表达式中出现空指针解引用或者悬空指针解引用，那么QCP的符号执行就必然无法从断言中找出相应的store谓词，此时，QCP符号执行器就会给出红色报错信息并退出。
当然，并不是所有上面提到的问题都会导致符号执行无法继续进行。例如，下面程序中进行了除法运算。
int arith(int x, int y)
/*@ Require 0 < x && x <= 100 && 0 < y && y <= 100
Ensure __return == x + y */
{
int t;
t = 1000 / x;
t = 10001 / (1001 - t * x);
y = x + y - t;
return y + t;
}
只要是除法运算就需要验证确保除数不为零。上面程序中，第一个除法的除数是x，很显然，由于Require条件中假设了0 < x所以该除法的除数必定不为零。这个推理是很容易的，QCP也确实能自动完成这一项推理。然而，哪怕QCP无法自动完成这项推理，其实这也不影响后续的符号执行，因为，QCP总是可以生成t = 1000 / x的符号执行结果如下，并用于后续的符号执行。
0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55)
其中x_58和y_55对应x与y在进入函数体时的初始值。而检查除数非零就变为一条验证条件：
0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
has_permission(&t) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
x_58 != 0
这也可以用简明分离逻辑断言写作：
0 < x@pre &&
x@pre <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
t == 1000 / x@pre &&
x == x@pre &&
y == y@pre
|--
x@pre != 0
像这样简单的验证条件QCP可以自动验证，而一些复杂的验证条件则不一定。可能一个验证条件本身是成立的但QCP无法自动确认完成验证。例如上述程序中的第二个除法运算，要保证其运算合法，就需要检验以下验证条件是否成立：
0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
1001 - (1000 / x_58) * x_58 != 0
这就是QCP生成的第二个验证条件。QCP无法自动检验其正确性，因而会生成黄色告警。但这不影响QCP后续的符号执行。
值得一提的是，C标准对于算数运算的合法性有着许多琐碎的约定，其中一些规定甚至对于不少软件开发人员来说是反直觉的。最具代表性的是：C标准规定有符号整数运算越界是未定义行为（undefined behavior），这某种意义上意味着，合法的C程序不应该包含有符号整数运算越界（无符号则无所谓）。QCP对于程序安全性的检查遵循了C标准的规定。因此，QCP在符号执行上面程序中的赋值语句t = 1001 / (1001 - t * x)时实际总共要生成下面三个验证条件：
0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
(10001 != -2147483648 || 1001 - 1000 / x_58 * x_58 != -1) &&
1001 - 1000 / x_58 * x_58 != 0
0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
1001 - 1000 / x_58 * x_58 <= 2147483647 &&
-2147483648 <= 1001 - 1000 / x_58 * x_58
0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
1000 / x_58 * x_58 <= 2147483647 &&
-2147483648 <= 1000 / x_58 * x_58
它们分别表示t = 1001 / (1001 - t * x)中的除法运算合法、减法运算合法以及乘法运算合法。