[klee-dev] (no subject)

Martin Nowack martin_nowack at tu-dresden.de
Thu May 15 08:48:57 BST 2014


Hey Davis,

Can you give me an example code?

I remember, once, I had the issue as well.
According to the code you can do the following: 
432  // NOTE: This assert may fire, it isn't necessarily a problem and
433     // can be disabled, I just wanted to know when and if it happened.
434     assert(0 && "FIXME: Unresolved direct target for a constant expression.”);

But try to insert the following code before the assertion and tell me if it works or the output before the assertion got triggered.

-------
    if (Function *f == dyn_cast<Function>(ce->stripPointerCasts()))
      return f;
   cs->dump();
———

Cheers,
Martin


On 15 May 2014, at 02:58, agan Davis <agandavis at gmail.com> wrote:

> Hi everyone
> 
> when I test some objects, it comes across the problem below:
> 
> klee: ModuleUtil.cpp:435: llvm::Function* klee::getDirectCallTarget(llvm::CallSite): Assertion `0 && "FIXME: Unresolved direct target for a constant expression."' failed.
> 0  klee            0x0000000000fde322 llvm::sys::PrintStackTrace(_IO_FILE*) + 34
> 1  klee            0x0000000000fdd749
> 2  libpthread.so.0 0x00002b0e978ffcb0
> 3  libc.so.6       0x00002b0e9855b425 gsignal + 53
> 4  libc.so.6       0x00002b0e9855eb8b abort + 379
> 5  libc.so.6       0x00002b0e985540ee
> 6  libc.so.6       0x00002b0e98554192
> 7  klee            0x00000000005ecf1c klee::getDirectCallTarget(llvm::CallSite) + 220
> 8  klee            0x00000000005cb712 klee::StatsTracker::computeReachableUncovered() + 258
> 9  klee            0x00000000005cce0b klee::StatsTracker::StatsTracker(klee::Executor&, std::string, bool) + 1291
> 10 klee            0x000000000059fc46 klee::Executor::setModule(llvm::Module*, klee::Interpreter::ModuleOptions const&) + 326
> 11 klee            0x000000000057ed62 main + 3794
> 12 libc.so.6       0x00002b0e9854676d __libc_start_main + 237
> 13 klee            0x00000000005969e9
> KLEE: watchdog exiting (no child)
> 
> Hoping someone give me help.
> 
> Thanks
> Davis
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

---------------------------------------------------
Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140515/4e9291f3/attachment.sig>


More information about the klee-dev mailing list