KLEE development status

[Mark R. Tuttle]

I'm a researcher at Intel trying to start a project applying KLEE to BIOS.

Is KLEE still under active development?

I see a lot of activity in the klee-dev archives, but KLEE itself seems to
require old versions of LLVM and STP, and I wondered what to make of that.
Is there support for MinGW? I see the MinGW binaries for llvm and llvm-gcc
version 2.9 under llvm.org, and I'm working on STP.

Thanks,
Mark

[Cristian Cadar]

Hi Mark, I'm glad to hear you're trying out KLEE at Intel. There is an
ongoing effort trying to upgrade KLEE to work with LLVM 3.4 (led by Dan
Liew and Martin Nowack, who could provide more details), but the changes
are non-trivial for full functionality. We would be of course happy to
get additional help here.

We don't target MinGW, and I'm not too familiar with it -- the core of
KLEE should not be too problematic, but the environment models assume a
POSIX-compliant environment, which might be an issue in MinGW.

Cristian

Post by Mark R. Tuttle
I'm a researcher at Intel trying to start a project applying KLEE to BIOS.
Is KLEE still under active development?
I see a lot of activity in the klee-dev archives, but KLEE itself seems
to require old versions of LLVM and STP, and I wondered what to make of
that. Is there support for MinGW? I see the MinGW binaries for llvm
and llvm-gcc version 2.9 under llvm.org <http://llvm.org>, and I'm
working on STP.
Thanks,
Mark
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Daniel Liew]

Post by Mark R. Tuttle
Is KLEE still under active development?

Yes it is :) . We do development on GitHub now.

Post by Mark R. Tuttle
I see a lot of activity in the klee-dev archives, but KLEE itself seems
to require old versions of LLVM and STP, and I wondered what to make of
that. Is there support for MinGW? I see the MinGW binaries for llvm
and llvm-gcc version 2.9 under llvm.org <http://llvm.org>, and I'm
working on STP.

Right now you can compile KLEE against LLVM 3.3 and use clang as the
bitcode compiler. We will soon be able to build against LLVM3.4 .
Right now building with LLVM 3.3 passes most of our test suite but
there issues relating to llvm intrinsics that have been added.

If you're making an effort to port STP please use upstream STP [1] and
not the r940 revision that the getting started page uses so that the
community can benefit from any work you do (assuming you want to open
source your changes). STP has changed quite a bit since r940
(different build system) so do not follow the STP build instructions
on the KLEE getting started page but follow the instructions in the
STP repository. Also be aware the upstream STP needs the boost C++
libraries.

[1] https://github.com/stp/stp

Thanks,
Dan.