hmmmm, i don't know of a good methodical way to debug this. one idea is to try to run with the following 2 options:
--write-cov (this will write a .cov file for each terminated state with the file/line info for any *new* lines that state has covered that previous states haven't ... make sure you compile your app with -g debug info to get file/line info) --only-output-states-covering-new=false (this will output ALL terminated states, not only those covering new lines ... this will cause Klee to output EVERY state that terminates, perhaps giving you some more indications of progress) fwiw, this searcher seems to work pretty well in practice (WAY better than default DFS) - it was used for the OSDI 2008 paper: --use-interleaved-covnew-NURS --randomize-fork --use-batching-search --batch-instructions 10000 --use-random-path here are some other possibly useful options used for OSDI 2008: --simplify-sym-indices --max-sym-array-size=100000 --max-memory=1000 --disable-inlining --use-forked-stp --use-cex-cache --with-libc --with-file-model=release --allow-external-sym-calls --exclude-libc-cov --optimize --output-module --max-instruction-time=10. --watchdog --max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1 --max-static-cpfork-pct=1 --switch-type=internal i think --use-cex-cache (counterexample cache) might help speed up things quite a bit. hope that was useful! best of luck. 2009/3/25 Raimondas Sasnauskas <raimondas.sasnauskas at cs.rwth-aachen.de> > Hello, > > Is there any way to localize the reason(s) for situations > where an application inside Klee does not make any progress? > > I'm running Klee with different path selection strategies, however, > the code I'm testing gets stuck for hours at some execution point in time. > CPU/memory usage remains constant and the `run.stats` keeps growing with > new entries. > Unfortunately, the output of my application does not really help me > to narrow down the blameworthy line(s) of code or maybe some complex > symbolic > constraints to be solved. > > The native binary runs without any problems. > > Thanks, > Raimondas > > > -- > Raimondas Sasnauskas, PhD Student > Distributed Systems Group > RWTH Aachen University > http://ds.cs.rwth-aachen.de/members/sasnauskas > > > > > > > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.Stanford.EDU > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20090325/8031c717/attachment.html
