struct int_pair {
int a;
int b;
};
Definition store_int_pair (p: addr) (x y: Z): Assertion :=
&(p # "int_pair" ->β "a") # Int |-> x **
&(p # "int_pair" ->β "b") # Int |-> y.
Sometimes, however, we want to keep the information about the structure inside a single store_int_pair predicate throughout verification, so that the assertions shown during symbolic execution stay compact. QCP also supports this behavior through customized assertion-transformation strategies.
Specifically, the user can add the following transformation strategy to the .strategies file:
id : 4
priority : post(1)
left : store(field_addr(?p, int_pair, a), I32, ?x) at 0
store(field_addr(p, int_pair, b), I32, ?y) at 1
action : left_erase(0);
left_erase(1);
left_add(store_int_pair(p, x, y));
The key word post is different from the earlier core examples. It means that this assertion transformation is performed automatically after symbolic execution of a memory read or write, rather than before symbolic execution in order to enable the read or write.
With this strategy, symbolic execution displays only the store_int_pair predicate throughout the verification of swap_int_pair, and the function no longer generates any VC that the user must manually prove.
After symbolically executing int temp = p->a, QCP obtains:
store_int_pair(p@pre, x, y) *
store_int(&temp, x) *
store_ptr(&p, p@pre)
After symbolically executing p->a = p->b, QCP obtains:
store_int_pair(p@pre, y, y) *
store_int(&temp, x) *
store_ptr(&p, p@pre)
After symbolically executing p->b = temp, QCP obtains:
store_int_pair(p@pre, y, x) *
store_int(&temp, x) *
store_ptr(&p, p@pre)
From this state, releasing the temporary variable temp and the local variable p directly yields the Ensure condition. Therefore QCP does not generate an additional VC that must be manually proved in Rocq.