Search code examples
llvmautotestklee

how does klee check verify the test pass or fail?


I have read the klee tutorial at Klee tutorial. It's pretty simple and straight forward. However, when I check files that generated by the test at KLEE generated files, I have not found any file tell me whether the test pass or fail? There could be two ways to verify the test results.

  1. KLEE is smart enough to know what's the expected return value of the 3 test cases

  2. KLEE simply dump the return value somewhere in a file and the human developer need to check them by themselves.

Is that so?


Solution

  • Klee won't give you the output to of your program running on the tests because it is analyzing your code statically (most of the times). so it's not actually running your program and that's why it's fast. If it wanted to run your program it would take a lot more time. You just need to run it yourself and see if the output is what you expected or not.

    Klee is a test input generation tool, not a test case generation tool. The difference is that a test case has both input and expected output.