Hi Brady, The -load option is indeed the right path.
The assertion you are hitting is probably something to do with an LLVM type KLEE doesn't have support for, most likely some kind of vector type. If you can get a small test case, please file a bug, it might not be too hard to fix. - Daniel On Tue, May 11, 2010 at 12:03 PM, <bgarvin at cse.unl.edu> wrote: > Hi, > > I'm trying to use klee on a subject that makes calls to the GMP and MPFR > libraries. ?These libraries use a lot of inline assembly, but I can > guarantee that their functions' arguments will always be concrete. > Therefore, I hoped to build GMP and MPFR as shared objects for x86_64 and > make them available to KLEE via the -load option. > > However, KLEE nonetheless complains about undefined references to > __gmp_version, __gmpz_add, etc. ?It subsequently aborts with an assertion > violation: > > Context.cpp:41: static unsigned int klee::Expr::getWidthForLLVMType(const > llvm::Type*): Assertion `0 && "non-primitive type argument to > Expr::getWidthForLLVMType()\n"' failed, > > which may be unrelated. ?As a sanity check, nm reports all of these > symbols appropriately defined and in their proper sections. > > Either I have misunderstood the -load option, or I have missed a step in > getting KLEE to find the symbols in the shared objects. ?My googling thus > far hasn't turned up much, except that KLEE may use libffi. ?Any > corrections to my understanding or pointers to documentation would be much > appreciated. > > Thanks, > Brady J. Garvin > > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
