This page links to the original bug reports that were made to the developers of different, compilers, and other software artifacts. These are all subtle bugs that are very hard to catch just through manual inspection (even after the tool points out the issue to you). The developers usually responded with thanks and fixed all these bugs promptly.
- Bug in ICC-16.03 involving integer overflow.
- This bug was found by our translation validator that checks equivalence between the generated binary and the original C program.
- Bug in ICC-16.03 related to incorrect reordering of memory accesses.
- This bug was found by our translation validator that checks equivalence between the generated binary and the original C program.
- Bug in GCC-4.8 involving incorrect reordering of memory accesses.
- This bug was found by our translation validator that checks equivalence between the generated binary and the original C program.
- Bug in Qemu machine emulator that is shipped with Linux/KVM hypervisor.
- This bug was found by our translation validator that checks equivalence between the generated PowerPC binary and the original x86 binary (in the context of Qemu's binary translator).
- Sorav Bansal was tipped bitcoins for this bug fix
- Three bugs in DietLibc, a C library for embedded systems (We describe one of the bugs below).
- All these bugs involve subtle interactions of the
charandinttypes. These bugs had escaped years of testing and production use. - The maintainer accepted these bug fixes with thanks. Abhishek Rose was acknowledged as a Dietlibc contributor by virtue of these fixes.
- Bug in the Yices SMT Solver
- This bug was found by differentially testing the output of one SMT solver against another during our verification runs for C programs.
- This bug report confirms that verification tools themselves are not immune to bugs. But it is usually possible to identify these bugs through simple testing, as we do in our tool.