ccadar/klee — pull request #68 by MartinNowack (2013-11-14 07:37:24+00:00)
Title: Feature klee internal functions

I was looking at the inlining of the checker functions. The goal was to avoid to use the instruction of a checker function to remember when a bug was already detected.

I think the current idea to solve it with inlining has some drawbacks:
* Modules (Kmodules) might grow quite large in case many checks are used
* Inlining of a function does not inline calls inside the inlined function which just allows simple check functions
* Debug information is not correctly propagated in general in KLEE when inlining happens due to the new handling of debug information in LLVM

(Tests failed with LLVM 3.3)

The current patches take a new approach:
Checker functions are marked as KLEE internal. In case a bug is detected during run time, KLEE crawls through the stack and finds the function which is not KLEE internal before the outermost KLEE internal function. This call instruction is used as the position information for the detected bug. Furthermore, this call gets debug information assigned from the instruction under check to correctly show where the bug is.

This way checker can be more complex and call different functions. In case of an error, the whole stack trace is provided but the correct position of the bug in the executed application is used.