Hi all, I have a question about KLEE. In the article "Symbolic Execution for Software Testing: Three Decades Later”[1], there is this quotation:
> Execution-Generated Testing (EGT): The EGT approach [9], implemented and > extended by the EXE [10] and KLEE [8] tools, works by making a distinction > between the concrete and symbolic state of a program. To this end, EGT in- > termixes concrete and symbolic execution by dynamically checking before every > operation if the values involved are all concrete. If so, the operation is > executed just as in the original program. Otherwise, if at least one value is > sym- bolic, the operation is performed symbolically, by updat- ing the path > condition for the current path. Could someone please point out to me where in the code the aforementioned “dynamic check” occurs? Looking at the tree as of commit d19500e, I would expect some kind of check before `executeInstruction` is called in `Executor:run()`, since `executeInstruction` appears to directly symbolically execute an LLVM IR instruction. However, I don’t see any kind of check like this. The article is from 2013, so please let me know if that quote isn’t accurate for the current state of KLEE. Thanks, Mark [1]: https://pdfs.semanticscholar.org/1144/3efe465ad544f478524da6c66c085b16e28b.pdf <https://pdfs.semanticscholar.org/1144/3efe465ad544f478524da6c66c085b16e28b.pdf>
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
