Re:C to Java Translation. Automatic, Complete, Correct. Free...
by danieltillett on Wednesday April 29, 2015 @09:09AM
(#9457979)
This sounds like a great spin off - bug finding in C code. Have you put much thought into pursuing this?
Re:C to Java Translation. Automatic, Complete, Correct. Free...
by marco2357 on Wednesday April 29, 2015 @09:24AM
(#9458066)
Didn't think too much about it since there are many C specific analyzers and tools that do the same. Well, they do it way better. E.g. Valgrind.
Re:C to Java Translation. Automatic, Complete, Correct. Free...
by danieltillett on Wednesday April 29, 2015 @09:34AM
(#9458124)
I would guess the value would be if you find bugs that other tools don't. If you just find the same bugs as Valgrind then I agree that there would not be too much value, but if you find unique bugs then it would be useful.
Translated applications still need to be thoroughly tested and usually some bugs are still found.
So we didn't formalize and verify our translation. Interestingly enough, we run into bugs in javac and ecj (Eclipse Java Compiler) surprisingly often. So verifying our translation would still lead to translations with bugs ;-)
Another fun fact: Since our translation knows the limits of allocated memory (and many other things), we found many illegal memory accesses in C programs that were unknown before (libgmp, micro httpd, vim, ...) since they didn't (or only very seldomly) lead to segfaults.