4 ms·
I think the LLVM level doesn't work as it throws away too much semantic information, but much of the CLANG front end can be used via it's API. There is a fork
by rjmunro 2y ago
I think the LLVM level doesn't work as it throws away too much semantic information, but much of the CLANG front end can be used via it's API.
There is a fork of CBMC called ESBMC that does this and many other changes: https://ssvlab.github.io/esbmc/documentation.html https://ssvlab.github.io/esbmc/documentation.html
- quotemstr 2y agoI'm curious about what relevant details get thrown away in translation to LLVM IR and that we can't add back with annotations. It's a shame that it's not possible to use these analysis tools on modern C++ codebases.
- rocqua 2y agoUndefined behavior around void pointers springs to mind.