Yes, it looks the same. I should be able to get to this in a couple weeks, ping 
me if you don't hear anything.

 - Daniel


On May 13, 2010, at 16:55, bgarvin at cse.unl.edu wrote:

> 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
>>> 
>> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev

Reply via email to