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
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 could help me!
Thank you.
Zhiyi Zhang
On Mon, May 25, 2015 at 3:16 PM, <[email protected]
<mailto:[email protected]>> wrote:
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 Zhang" <[email protected]
<mailto:[email protected]>> wrote:
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 or nurs:depth, KLEE runs OK.
2, Why KLEE uses "interleaved" searcher? Is
"interleaved"search heuristic better than single
search heuristic for symbolic execution?
Best wishes!
Zhiyi Zhang,
On Mon, May 25, 2015 at 5:20 AM, Sean Bartell <[email protected]
<mailto:[email protected]>> wrote:
Zhiyi Zhang on 2015-05-24:
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 the only path search heuristic,
KLEE also does NOT generate test cases. I am confused
why this phenomenon happens?
How does it fail? Does it crash with an error message, or
does it just keep running without printing anything?
2, The default search heuristic for KLEE is "random-path
interleaved with nurs:covnew". What is the meaning of
"interleaved"? Does it mean randomly selecting one
search heuristic from such two search heuristics when
searching a path?
Yes, except that it isn't random. The "interleaved" searcher
just alternates between using two other searchers.
"nurs:covnew" and other searchers can always choose a state.
_______________________________________________
klee-dev mailing list
[email protected] <mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
