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
