以下三个C函数都是取绝对值的潜在实现方法。这里我们仅仅举例说明验证它们的一个简单性质：如果调用它们时的参数不为INT_MIN，那么它们就能安全运行，并且其返回值非负。
int abs0(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
Ensure __return >= 0 */
{
if (x < 0) {
return - x;
}
else {
return x;
}
}
int abs1(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
Ensure __return >= 0 */
{
if (x < 0) {
x = - x;
}
return x;
}
int abs2(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
Ensure __return >= 0 */
{
if (x > 0) {
return x;
}
return - x;
}
if语句的符号执行
以其中abs0函数的符号执行为例，它的符号执行是从“进入函数体”开始的，这一初始步骤生成的断言是：
INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
如果后续x的值发生变化，那么这个x_30可以被看作x@pre。如果x的值还未发生变化，那么这个x_30就既是x的初始值又是x的当前值。
接下去要符号执行的是if语句，该语句的判定条件是x < 0这一表达式。QCP的符号执行模块会发现，当x_30 < 0时，这个条件为真，当x_30 >= 0时，这个条件为假。因此，符号执行器会为该if语句的两个分支分别生成一个断言，if-true分支得到断言
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
而if-false分支（即else分支）得到断言
x_30 >= 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
当在IDE中将光标指向if-true分支的开头时，按Ctrl+Right快捷键可以看到当前分支的符号执行结果：
return语句的符号执行
在if-true分支中，abs函数会返回- x。这个C表达式- x的值就是- x_30。QCP的符号执行模块会分两步完成该return语句的符号执行。首先是符号计算出将要返回的数值：
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && __return == - x_30 && store_int(&x, x_30)
其次是释放局部变量（含形参）所占据的内存空间：
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && __return == - x_30
由于x_30表示的是形参x的初始值，这个return断言也可以写作以下形式：
x@pre < 0 && INT_MIN < x@pre && x@pre <= INT_MAX && __return == - x@pre
值得一提的是，IDE给出反馈时，右边栏将此断言列为Return断言，而非我们之前见到的Normal断言。它的意思是，即将在一个符合该断言的程序状态上退出该函数体的执行，而非要基于这个程序状态继续执行当前光标处之后的程序。
符号执行进入if-false分支的情形
当在IDE中，将光标指向if-false分支的开头时，按Ctrl+Right快捷键可以看到当前分支的符号执行结果：
此时IDE会同时显示当前分支的Normal断言以及先前分支的Return断言。如前面提到的那样，当前分支的Normal断言用基本分离逻辑断言和简明分离逻辑断言表述分别是：
x_30 >= 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
x@pre >= 0 && INT_MIN < x@pre && x@pre <= INT_MAX && x == x@pre
在此基础上符号执行return x语句会得到
x@pre >= 0 && INT_MIN < x@pre && x@pre <= INT_MAX && _return == x@pre
这也是Return断言，IDE此时会把两条Return断言收集在一起显示。
if语句结束后的情形
在abs0函数的if语句两分支都是return语句，因此程序本就不会执行到if语句之后的部分（当然，这条if语句之后也没有别的语句了），相应的，如果查看if语句结束后的符号执行结果，其仅包含两条Return断言，而没有Normal断言。
退出函数体时要检查的条件
在推出函数体时，QCP会检查是否所有的Return断言都能推出Ensure条件。就abs0而言，就需要证明以下两条性质：
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && __return == - x_30 |-- __return >= 0
x_30 >= 0 && INT_MIN < x_30 && x_30 <= INT_MAX && __return == x_30 |-- __return >= 0
QCP会确认，这两条数学推导确实成立。至此，QCP就完成了abs0函数的验证。
abs1函数的符号执行
abs1函数与abs0函数稍有不同。它的if语句只有一个分支，并且其中只有普通赋值语句而没有return语句。
int abs1(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
Ensure __return >= 0 */
{
if (x < 0) {
x = - x;
}
return x;
}
当QCP符号执行到if-true分支结束时，符号执行的结果是一个Normal断言，而不是之前abs0中的Return断言。其使用基本分离逻辑断言和简明分离逻辑断言分别可以如下表述（其中x_30和前面一样对应x@pre）：
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, - x_30)
x@pre < 0 && INT_MIN < x@pre && x@pre <= INT_MAX && x == - x@pre
在工具中，可以看到如下反馈信息：
在if语句结束之后，QCP的符号执行会收集将两个Normal断言收集起来（包括没有出现的if-false分支断言），用基本分离逻辑断言写出就是：
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, - x_30)
x_30 >= 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
用简明分离逻辑断言写出就是：
x@pre < 0 && INT_MIN < x@pre && x@pre <= INT_MAX && x == - x@pre
x@pre >= 0 && INT_MIN < x@pre && x@pre <= INT_MAX && x == x@pre
当然，如果要在工具中让IDE显示这些符号执行的结果，那么会遇到一些小麻烦。原因是abs1的if语句没有else分支，但是当光标停在if-true分支结束处时，工具并不知道后续是否还有else分支，因此QCP工具此时只会显示if-true分支的结束条件。
要让工具同时显示两个分支的符号执行结果（相当于整个if语句的符号执行结果）可以手动添加一个空的else分支。
当然，无论有没有把这个空的else分支写出来，QCP都会基于两个分支的汇总继续后续的推理。就abs1函数而言，QCP推导return x的符号执行结果时，会根据前面的两条Normal断言得到两条Return断言。
当然，这两条Return断言都能推出Ensure条件，至此QCP也完成了abs1的验证。
abs2函数的符号执行
abs2函数又与前两个函数不同。
int abs2(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
Ensure __return >= 0 */
{
if (x > 0) {
return x;
}
return - x;
}
它的if-true分支是一个return语句，其符号执行会产生一个Return断言。它没有if-false分支，相当于这个分支为空，会产生一个Normal断言。要在工具中查看整个if语句的符号执行结果，还是需要像前面一样手动添加一个空的else分支。
这两个断言中只有Normal断言会由于后续语句的符号执行。最终，在return - x之后的符号执行结果如下：
