Question to devs who've also written parsers:

Is this a lame bug?

I have never written formal verifications for code, or had to apply concepts like "Verified Design-by-Contract", but I have written parsers, scanners and lexers. In all honesty, the most important part of the httpd is "parsing" requests. I have had chats with Igor, the main developer of Nginx, related to performance tuning and the kernel TCP/IP stack. I must tell that he's a really nice guy. But, if it was my "main job" to write a software used by millions of people, which has an achilles heel in it's parser, then I'd sit down and teach myself to prove the parser code. I have researched this 2y ago, and found that you can quite professionally write BDD/TDD style tests and mocks in C99 too. The tools available go way beyond that though.

Here's a little list of things I have found useful back then:

http://frama-c.com/ (this was top notch)

http://gulliver.eu.org/free_software_for_formal_verification

I want to name: http://www.eschertech.com/products/index.php and http://research.microsoft.com/en-us/projects/vcc/ too, but I haven't tested any of these tools, because I never worked in an environment where my code had to go through formal verification.