ITADN

Ghost update program instrumenter

#1999Openmichael-schwarz 创建于 2026-04-14
ghost-branch
M
michael-schwarzcommented
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 条评论