[klee-dev] Path Search Heuristics

[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
> 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, <gwpublic at wp.pl
> <mailto:gwpublic at wp.pl>> 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" <xianlingzibiying at gmail.com
>     <mailto:xianlingzibiying at gmail.com>> 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 <sean at yotann.org
>         <mailto:sean at yotann.org>> 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
>         klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>         https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>