Hello, I have a few questions about KLEE and I batched them in this email.
- When using the file model, are the modeled calls allowed to work with concrete files? From reading the current snapshot of the code it seems this is not true, for instance ioctl is only allowed for symbolic files, else it returns an error. - I got the memory error "unbound pointer" when I mixed the symbolic file system and allowed some syscalls to go through the OS. I assume this is due to the fact that memory is modified outside of the KLEE environment. It also happens when the code calls into a native library. To go around it, I usually compile all dependencies with klee- gcc but for instance, for libX11, there are a lot of dependencies ;) I was wondering if you see an alternative to this, such as making KLEE aware of the memory object even if it was allocated by a native library. - Currently KLEE does not support inline assembly and it is sometimes too complicated to rewrite all asm functions. Do you think there could be a way to execute inline asm, pretending for instance that it is an external call? - Are the statistics used by the StatsTracker used in any of the the searchers? How will the search perform without these statistics? - Did you see in practice any implications from the the warning "this target does not support llvm.stacksave intrinsic"? - Do you have any experience with the LLVM/CLANG static analyzer? Would it be a good framework to perform static analysis on LLVM bytecode and use it for instance to maximize code coverage under KLEE? We are currently doing this more or less "manually" but it would be great to have a better framework. First of all, is the analysis done on LLVM bytecode? I am guessing no, since C++ would then be easy to support, however it is not fully supported yet by the CLANG static analyzer. - There are two new interns helping out with KLEE in our lab, could you please add them as well to the klee-dev list? There emails are liviu.ciortea at epfl.ch and vlad.georgescu at epfl.ch Hope I didn't batch too many questions ;) Thank you very much, Cristi
