[klee-dev] How to Reduce the Number of .ktest Files Generated by KLEE

Sun shutong255 at gmail.com
Mon Jul 8 00:24:05 BST 2024


Dear KLEE Community,
I am currently working on a project using KLEE, and I have encountered an issue with the number of .ktest files generated during the execution. Specifically, my project generates a large number of .ktest files, which is not efficient for my needs. I am looking for a way to limit the number of .ktest files generated to only the top 10 longest paths based on the number of instructions executed.
Here is what I have attempted so far:

  1.  I modified the Executor.cpp file to track the number of instructions executed for each path.
  2.  I attempted to implement a priority queue to keep track of the top 10 longest paths.
  3.  I tried to modify the shouldWriteTest function to only write .ktest files for the longest paths.

However, my current implementation results in a segmentation fault, and I am not sure if my approach is correct.
Could you please provide guidance on the following:

  1.  Is there an existing way to limit the number of .ktest files generated by KLEE?
  2.  If not, what would be the best approach to modify the KLEE source code to achieve this?
  3.  Any specific functions or parts of the codebase that I should focus on to implement this feature?

Thank you for your time, best regards,
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list