3 ms·
Let's say you want to check if use after free can ever occur. Your translation is bugged and translates the whole program to a single "nop". Then the verifier h
by im3w1l 2y ago
Let's say you want to check if use after free can ever occur. Your translation is bugged and translates the whole program to a single "nop". Then the verifier happily asserts that the translated program does not cause use after free.
I doubt the translation would be that bad but it could have more subtle issues of the same kind.
- bennofs 2y agoMy argument is that you typically also check other properties, like properties describing what your program should do. These other properties likely wouldn't be satisfied by a nop program, and hopefully the same is true for many subtle issues.