[klee-dev] Using klee with LLVM 3.3 + Clang

[Martin Hořeňovský]

Hello,

after seeing a series of patches  for LLVM 3.3 compatibility on git, I
wanted (or rather, I am unsuccessfully trying to) build Klee against
current LLVM and Clang. However, I am currently having trouble compiling
Klee as it gives *No rule to make target ../**klee_div_zero_check.ll **needed
by ../klee_div_zero_check.bc *error. Searching through the internet and
this mailing list tells me that this is caused by not having llvm-gcc in
path (or rather, not having it used in compiling llvm, which means that the
makefile doesn't know it exists, leading to klee makefile not knowing it
exists and failing). Problem with that is that, as far as I can tell,
current LLVM makefile doesn't care about llvm-gcc and doesn't set it as a
variable even if given.

My question is twofold
a) Is there a plan to move over to LLVM 3.3 in near future, or at least
modify the build system to make using newer LLVM versions less painful?
b) Can anyone help me (or point me in the right direction) with modifying
the makefiles so that building Klee becomes possible?

Best regards
Martin Horenovsky


Also, for a sanity check, here is what I did and tried while building so
far:
1) Bootstrapped and checked LLVM+Clang 3.3 in Release mode. (So that LLVM
would have clang set as it's compiler)

2) Built STP from the git repository announcement that went through this
mailing during September. (As far as I can tell, I set it up with CMake to
be ~equivalently set up with the what the tutorial says.)

3) Built uclibc. To my surprise its configure script was unable to function
when called out of tree, but after some quick finagling, it (as far as I
can tell) compiled ok. (btw, is it under any kind of active development? I
think I've seen talk about adapting a new version of uclibc and then
keeping that one currentish. If it is, I would probably send at least a
quick patch to configure)

4) (Tried to) build Klee. At first it threw out couple of errors saying
that it doesn't have any compiler set, so I just set
the appropriate variable in makefile to clang/++. Then it proceeded a bit
but threw the above mentioned error. So I have then tried to add what seems
to be the llvmgcc path variable to the llvm makefile, but nothing has
changed.
-------------- next part --------------
HTML attachment scrubbed and removed