Ghost update program instrumenter
ghost-branch
Given the ghost update provided in a YAML witness, insert these into the CIL program representation according to the location information provided in the witness. The ghost update and the statement that precedes it should be turned into the following fragment:
~~~C
__VERIFIER_atomic_begin();
originalstatement;
ghostupdate;
__VERIFIER_atomic_end();
~~~
Produce a CRAM test that verifies that the placement is correct.
0 条评论