Hi Philip, Thanks a lot for the CDE package, it's really helpful. I just added your instructions to the Getting Started webpage.
Best, Cristian On 26/05/2011 00:42, Philip Guo wrote: > 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 > <mailto: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/.) > > > > > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
