Daniel, The switch statement in getWidthForLLVMType(llvm::Type t) is seeing t->getTypeID() as 10, which LLVM's Type.h maps to llvm::Type::StructTyID. That leads me to suspect that I am seeing http://llvm.org/bugs/show_bug.cgi?id=6171. I'll see what I can do to contribute to this bug report.
Thanks, Brady > 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 >> >
