Re: [klee-dev] Path Search Heuristics

2015-05-27 Thread Cristian Cadar
Hi, please open a new issue on GitHub and include a small example demonstrating this problem. Also, as documented in the code, you can try to disable this assert. Cristian On 27/05/15 05:42, Zhiyi Zhang wrote: Hi, all I have found the error report when I only used search==nurs:covnew as

Re: [klee-dev] Path Search Heuristics

2015-05-27 Thread Sean Bartell
Zhiyi Zhang on 2015-05-27: I have found the error report when I only used search==nurs:covnew as the path search heuristic. It is klee: ModuleUtil.cpp:435: llvm::Function* klee::getDirectCallTarget(llvm::CallSite): Assertion `0 FIXME: Unresolved direct target for a constant

Re: [klee-dev] Path Search Heuristics

2015-05-26 Thread Zhiyi Zhang
Hi, all I have found the error report when I only used search==nurs:covnew as the path search heuristic. It is klee: ModuleUtil.cpp:435: llvm::Function* klee::getDirectCallTarget(llvm::CallSite): Assertion `0 FIXME: Unresolved direct target for a constant expression.' failed. Hope somebody

Re: [klee-dev] Path Search Heuristics

2015-05-25 Thread gwpublic
It's explained in paper, Also for exercise I recommend you to try to explore graph of possible states of few simple programs (some execution path leading to infinite loop, recursion) and you should see where things can keep exploring indifinitely. All the best! Greg On 25 May 2015 07:42, Zhiyi

[klee-dev] Path Search Heuristics

2015-05-24 Thread Zhiyi Zhang
Hi all, I have some questions about path search heuristics used in KLEE. 1, It seems that KLEE can NOT generate test cases when I only used search==nurs:covnew as the path search heuristic. Moreover, when using search==nurs:md2u, search==nurs:icnt, search==nurs:cpicnt or search==nurs:qc as as

Re: [klee-dev] Path Search Heuristics

2015-05-24 Thread Zhiyi Zhang
Hi Bartell, Thanks for your reply very much. 1, KLEE keeps running without printing anything. I set KLEE running time for one hour, but it stops very quickly. There is no error reports. In the klee-out folder, there are only assembly.ll and run.stats files. However, when I used bfs, dfs, random