With the help of Cristian, I've put together an improved version of the Klee
package:

http://keeda.stanford.edu/~pgbovine/klee-cde-package.v2.tar.bz2 (200MB)

Now you're able to run the Klee regression tests AND also replicate the
world-famous coreutils case study from:
http://klee.llvm.org/TestingCoreutils.html

See the README file in the package for detailed instructions.


On Wed, May 25, 2011 at 11:47 AM, Philip Guo <pg at cs.stanford.edu> wrote:

> Hi everyone,
>
> I'm helping someone who's struggling to compile Klee right now, and I've
> used my CDE tool (http://www.stanford.edu/~pgbovine/cde.html) to create a
> completely self-contained package so that new Klee users can get
> up-and-running without first installing any of its pesky dependencies.  The
> package is 151MB and located here:
>
> http://keeda.stanford.edu/~pgbovine/klee-cde-package.v1.tar.bz2
>
> Feedback and testing would be greatly appreciated :)
>
> Daniel - if you think this is useful, that would be awesome to get this
> uploaded to the official Klee webpage.
>
> Thanks,
> Philip
>
>
> Here is the README file from the package:
> ---
> This package contains a self-contained distribution of Klee and all of
> its associated dependencies (e.g., llvm-2.7, llvm-gcc, uClibc, svn).
> Using this package, you can:
>
> 1.) Compile target programs using llvm-gcc
> 2.) Run Klee on target programs compiled with llvm-gcc
> 3.) Hack on Klee's source code and re-compile it to build a new Klee binary
> 4.) Pull the latest Klee source code updates from SVN
>
> ... all without compiling or installing anything on your Linux machine!
>
> The only requirement is that you are running a reasonably-modern
> x86-Linux distro that can execute 32-bit ELF binaries.
>
> ---
>
> Instructions:
>
> 1.) Compile a target program using llvm-gcc
>
> I've put an example program in:
>   cde-root/home/pgbovine/test-programs/islower.c
>
> To compile it into LLVM object code, run:
>
>   cd cde-root/home/pgbovine/test-programs/
>   ./llvm-gcc.cde -I../klee/include --emit-llvm -c -g islower.c
>
> This will create a file called islower.o, which is ready to be run
> through Klee.
>
>
> 2.) Run Klee on the compiled target program
>
>   cd cde-root/home/pgbovine/test-programs/
>   ./klee.cde islower.o
>
> This should create klee-out-* and klee-last sub-directories, which
> contain the output of Klee from running on islower.o
>
> To see all of the myriad of Klee options, run:
>   ./klee.cde --help
>
>
> 3.) Hacking on Klee source code
>
> The Klee source code is located in: cde-root/home/pgbovine/klee/
>
> You can freely edit the source code, and then to compile, run:
>   cd cde-root/home/pgbovine/klee/
>   ./make.cde
>
> (Note that running your system's native 'make' will NOT work; you must
> run make.cde!)
>
> This will create a new Klee binary in:
>    cde-root/home/pgbovine/klee/Release+Asserts/bin/klee
>
>
> ("./make.cde clean" doesn't seem to work too well right now, though.)
>
>
> 4.) Updating to the latest Klee source from SVN
>
> cd cde-root/home/pgbovine/klee/
> ./svn.cde up
>
> (Note that running 'svn' might not work if you have an incompatible
> version of SVN installed, but './svn.cde' should always work since it
> runs the version of svn in the package, which exactly matches the format
> of the .svn/ directories within cde-root/home/pgbovine/klee/.)
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: 
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110525/a08face5/attachment.html
 

Reply via email to