Hi, > I want to explore symbolic execution and KLEE seems like a good choice for > beginning. But I would like you guidance in getting to know the best way to > understand the code of KLEE.
One thing you certainly do is read the OSDI'08 paper on KLEE to get a high level understanding of what it tries to do. One approach you could take to trying to understand the code is by trying to run a simple closed world (i.e. makes no external calls) program that contains no symbolic variables and does not link in any libraries (i.e. do not use --posix-runtime or --libc=...). Once you understand what KLEE has done by looking at the output files (e.g. assembly.ll) you could try following what KLEE is doing by running through gdb and break at points of interest and then following through what KLEE does. If you succeed in doing that try introducing a symbolic variable in your simple closed world program and running through gdb and see how KLEE behaves. This requires that you learn how to use gdb or use it indirectly via an IDE like Eclipse (with the CDT plug-in). It will certainly take time to learn this but IMHO it's worth the effort. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
