What every C Programmer should know about undefined behavior #2/3 [LWN.net]

What every C Programmer should know about undefined behavior #2/3

Posted May 17, 2011 5:26 UTC (Tue) by cmccabe (guest, #60281)
In reply to: What every C Programmer should know about undefined behavior #2/3 by wahern
Parent article: What every C Programmer should know about undefined behavior #2/3

Klee is cool; thanks for sharing that. To be fair, though, it's not a tool for proving programs correct; it's a tool for generating lots and lots of test cases automatically.

There was another tool for Ruby that would randomly alter your code at runtime (!) and see how you handled the resulting errors. I am having a really hard time remembering the name, though...

What every C Programmer should know about undefined behavior #2/3

Posted May 17, 2011 18:35 UTC (Tue) by wahern (subscriber, #37304) [Link]

Correct me if I'm wrong, but symbolic execution engines are what you get when you don't allow the halting problem to dissuade you from analyzing the code, and KLEE is a symbolic execution engine that generates test cases for interesting paths that it has deduced, such as paths to a bug. If a program is small enough KLEE can find many paths which result in the termination of the program, but for large applications KLEE can run for hours or days. In fact, it could run forever, AFAIU, if its heuristics don't terminate the algorithm. This is why it allows you to specify different starting points so you can get complete coverage over more interesting sub-components of an application.