[klee-dev] Path Search Heuristics

[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 expression."' failed.

There are a few things you can try:

1. Add the `-optimize` option when you run KLEE. That may optimize out the 
   bitcode triggering the assertion.
2. Apply [my 
   patch](https://github.com/yotann/klee/commit/dff4069042e6f7b4bc7211b8e9ba3377ee01c33c) 
   that fixes the assertion in certain cases.
3. Modify KLEE to call `ce->dump()` right before the assertion, which will 
   print out the value that causes the problem.
-------------- next part --------------
HTML attachment scrubbed and removed