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. I think the --load option is used by LLVM to load plugins. I never tried it but it should work, perhaps others have experience with this option. Another option, which I remember worked in the past, is to use llvm-ld to link in the shared library too. You may use llvm-nm in this case to check if the symbols are defined. > 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, I think these are unrelated indeed. You can investigate further and see which is the type that fires this assertion and what is the width of the type. I suspect this is something specific to 64bit. Cristi > > 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
