[klee-dev] Klee Make Check

[Ben Mehne]

Hello,

I am trying to compile and use Klee with the POSIX/uClibc environment, but
"make check" exits with error and "Unexpected Failures: 36".  Does this
mean that klee will not function as intended?  Any guidance would
appreciated.

-- My Setup
I am building Klee using stp r940 with the patches from this mailing list
(and its git), LLVM 2.9 with the unistd.h patch, and trunk Klee.  "make
unittests" does not exit with error.  I am using the attached build_klee.sh
script (if it is not scrubbed - it is just the directions from the wiki +
patches in a bash script).  As far as I can tell, the llvm-gcc is being
used wherever a compiler is needed in klee and llvm-2.9.  I am on 64 bit,
Arch Linux; I have GCC 4.9.2 installed, and llvm 3.6, but I think if those
were the problem, the issue would be during compilation, not running tests.

-- Bug/Issue Details
All of the unexpected failures (unless I missed one) exit on the assert:
klee: main.cpp:1109: llvm::Module* linkWithUclibc(llvm::Module*,
llvm::StringRef): Assertion `ft->getNumParams() == 7' failed.  All test
cases that call this function fail.

This is failing because the FunctionType has no params and is variable args
as per the getOrInsertFunction on line 1025.  This leads me to believe that
either the bca file that is being linked in is corrupt/wrong or there is
some deep bug in the LLVM 2.9 code that links it in.  Attached is the bca
file (if it has not been scrubbed).  The archive file does seem to have
"__uClibc_main" defined in __uClibc_main.os .

I notice that the travis build system does not run "make check" - could it
be a subtle compilation issue with llvm-2.9?

Thank you for your help,
-Ben Mehne
-------------- next part --------------
HTML attachment scrubbed and removed
-------------- next part --------------
A non-text attachment was scrubbed...
Name: build_klee.sh
Type: application/x-shellscript
Size: 7010 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150522/db1a5550/attachment.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: libklee-libc.bca
Type: application/octet-stream
Size: 24700 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20150522/db1a5550/attachment.obj>