I've not used the CDE build of KLEE but based on the error message it sounds like either there is a problem with the version of LLVM that is used for the CDE build of KLEE or something is wrong with your generated LLVM bitcode file that you're trying to symbolically execute.
How exactly are you generating the islower.o file? Can you symbolically execute the file I've generated here ( http://www.doc.ic.ac.uk/~dsl11/islower.o )? It definitely works with my version of KLEE. Regards, Dan Liew. On 12 August 2012 11:09, Qiuping Yi <[email protected]> wrote: > Hi, I use klee-cde-package now, when I use klee.cde to symbolically > execute a .o file, I get the following error, what's wrong? > > /islower$ ../../../../../../bin/klee.cde islower.o > klee: BitcodeReader.cpp:795: bool llvm::BitcodeReader::ParseMetadata(): > Assertion `0 && "Inavlid Named Metadata record"' failed. > 0 klee 0x08965ab8 > +++ killed by SIGABRT (core dumped) +++ > Aborted (core dumped) > > > _______________________________________________ > klee-dev mailing list > [email protected] > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
