[klee-dev] coreutils on KLEE3.4

Dan Liew dan at su-root.co.uk
Wed Mar 18 08:57:04 GMT 2015


Hi Zhiyi,

Please do reply-all when using the mailing list so that klee-dev gets CC'ed.

On 18 March 2015 at 08:32, Zhiyi Zhang <xianlingzibiying at gmail.com> wrote:
> Hi Dan,
>
> Thank you for your reply very much.
>
> I am still confused that do you mean coreutills cannot be run on KLEE
> compiled with
> LLVM 3.4, expect I use the whole-program-llvm?

No.

I am saying

- ``klee-gcc`` is just a wrapper script (read the code) for ``llvm-gcc``.

- ``llvm-gcc`` will emit LLVM bitcode in the format used by LLVM 2.9.

- KLEE supports being built with different versions of LLVM.

- You have built KLEE with LLVM 3.4 therefore you cannot use
``llvm-gcc`` (the LLVM bitcode will be incompatible) therefore you
cannot
use the ``klee-gcc`` wrapper script.

You have three options

* Use whole-program-llvm. This is what I would advise.

* Use ``klee-clang`` [1] which is wrapper script around clang.

* Use KLEE with llvm 2.9, llvm-gcc and the klee-gcc wrapper script.



[1] https://github.com/klee/klee/pull/213



More information about the klee-dev mailing list