[klee-dev] choose concrete path

Martin Nowotny martin.nowotny at student.tugraz.at
Wed Jul 2 07:28:49 BST 2014


Hello everyone,

I have a problem using seeds with klee.
What I want to accomplish is, to get a particular path through my 
program, therefore I use a modified .ktest File and read that file in 
with the commandline argument --seed-out=testfile.ktest.

Now the .ktest file is read in, but it seems that anyhow klee is not 
using that given seeds. Because in my point of view the
void Executor::run(ExecutionState &initialState) recognizes the given 
seeds (usingSeeds is true), but does not do anything with them?
I already searched in the Newsarchive for an answer to my problem, it 
seems that there was already an issue about that [1][2]. Unfortunately 
it is not explained further.
Would anybody be so kind and help me, what to do?

Thank you very much,
Martin

[1] http://www.mail-archive.com/klee-dev%40imperial.ac.uk/msg00874.html
[2] http://www.mail-archive.com/klee-dev%40imperial.ac.uk/msg00688.html




More information about the klee-dev mailing list