[klee-dev] Path Search Heuristics

[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 could help me!
Thank you.
Zhiyi Zhang

On Mon, May 25, 2015 at 3:16 PM, <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> 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> 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
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
-------------- next part --------------
HTML attachment scrubbed and removed