Hi,
On Tue, 11 Jun 2024 11:41:34 +0000 Sun <shutong...@gmail.com> wrote: > When running Klee on various programs, I notice that it generates a > `.ktest` file for each explored execution path. For my current > project's scope, this behavior results in excessive data, most of > which is not relevant to my needs. Specifically, I am interested in > only retaining the `.ktest` files for the ten longest execution > paths, which are most relevant to my analysis. typically one would use, e.g.: --only-output-states-covering-new to reduce the number of generated ktest files. > Could you please advise: > 1. Is there an existing command-line option or configuration setting > in Klee that allows for limiting the generation of `.ktest` files to > only the longest paths? > 2. If no such setting exists, could you point > me towards the parts of Klee's source code where modifications might > be implemented to achieve this functionality? How would you now the lengths of the longest paths in advance? You could modify shouldWriteTest in the Executor: https://github.com/klee/klee/blob/ad557cb0f8e20a0e4a86ea5fcd11ed95f5c3b637/lib/Core/Executor.cpp#L3788 The depth is in the ExecutionState: https://github.com/klee/klee/blob/ad557cb0f8e20a0e4a86ea5fcd11ed95f5c3b637/lib/Core/ExecutionState.h#L180 Kind regards, Frank _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
