Hi there, I am experiencing concolic execution with KLEE recently. Here is what I want to achieve. I record the path by giving KLEE a concrete file input. The -output-paths option will generate path files in klee-output folders. Then, I want to replay the path but give KLEE a symbolic file input. At the end, I want to get the symbolic path constraint that would generate the path.
I find there is discordance between the paths. So I need some help with KLEE. First, I want to output the llvm assembly code at each node of path. In this way, I can know where they diverge and try to reconcile the concrete-run and symbolic-run paths. (My theory is that the code diverge inside libc functions) Second, I created an empty main function and compiled it to bytecode a.bc. When I run $klee ... a.bc <concrete file>$ and $klee ... a.bc A --sym-files...$ I would get different path files. What would be the reason for that? Thank you, Zekun Shen
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
