A complicating factor is that you really should include your compiler as part of your codebase (if you're doing lots of formal method work, you will usually do it on the source code, and the compiler can invalidate all of the guarantees you carefully program in), and this will be millions of lines of code (where you can't simply factor a tonne out).

Think GCC 5 is about 15 million or so now.