The QCP tool allows users to add assertion annotations between program statements to assist in completing verification. The loop invariant mentioned earlier is one such type of assertion annotation. When the QCP symbolic executor encounters an assertion annotation, it checks whether the strongest postcondition previously obtained through symbolic execution can entail the assertion manually provided by the user. Let us use the previously introduced swap function as an example.
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;
}
After the first assignment statement executes, the program state satisfies the following assertion (which is also the strongest postcondition obtained by the QCP symbolic executor):
store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)
Here, px_37 and py_40 represent the initial values px@pre and py@pre. Of course, looking at the subsequent program, we know that the value currently stored in * px is not needed. Below, we assert a weaker property at this program point.
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;
/*@ Assert
store_int(&t, x) *
store_ptr(&px, px@pre) *
store_ptr(&py, py@pre) *
has_int_permission(px@pre) *
store(py@pre, y) */
* px = * py;
* py = t;
}
Adding this assertion means "the program state must satisfy this property when execution reaches this point," and the correctness of subsequent program statements is guaranteed solely by this property. In other words, even if we can actually prove that a stronger property holds when execution reaches this point, the verification of subsequent program statements does not need that stronger property. Therefore, when QCP encounters such an annotated program during verification, it generates a verification condition (VC) like the following (which requires verifying that the assertion on the left of |-- can entail the assertion on the right of |--), and then performs subsequent symbolic execution based on the user-provided assertion.
store_int(&t, x) *
store_ptr(&px, px@pre) *
store_ptr(&py, py@pre) *
store_int(px@pre, x) *
store_int(py@pre, y)
|-- store_int(&t, x) *
store_ptr(&px, px@pre) *
store_ptr(&py, py@pre) *
has_int_permission(px@pre) *
store_int(py@pre, y)
The two figures below show the comparison before and after symbolic execution of this assertion. After symbolic execution of the assertion, the Normal assertion list displays the has_permission predicate introduced by the assertion annotation.
