Martin Nowotny
2014-07-02 06:28:49 UTC
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
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